SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>Primitive recursive function</title>

</head>

Primitive recursive function

</h1>

</header>

In <a href="Computability_theory" title="Computability theory">computability theory</a>, a primitive recursive function is, roughly speaking, a function that can be computed by a <a href="Computer_program" title="Computer program">computer program</a> whose <a href="Loop_(programming)" class="mw-redirect" title="Loop (programming)">loops</a> are all <a href="For_loop" title="For loop">"for" loops</a> (that is, an upper bound of the number of iterations of every loop is fixed before entering the loop). Primitive recursive functions form a strict <a href="Subset" title="Subset">subset</a> of those <a href="General_recursive_function" title="General recursive function">general recursive functions</a> that are also <a href="Total_function" class="mw-redirect" title="Total function">total functions</a>.

The importance of primitive recursive functions lies in the fact that most <a href="Computable_function" title="Computable function">computable functions</a> that are studied in <a href="Number_theory" title="Number theory">number theory</a> (and more generally in mathematics) are primitive recursive. For example, <a href="Addition" title="Addition">addition</a> and <a href="Division_(mathematics)" title="Division (mathematics)">division</a>, the <a href="Factorial" title="Factorial">factorial</a> and <a href="Exponential_function" title="Exponential function">exponential function</a>, and the function which returns the nth prime are all primitive recursive.<a href="#cite_note-FOOTNOTEBrainerdLandweber1974-1">[1]</a> In fact, for showing that a computable function is primitive recursive, it suffices to show that its <a href="Time_complexity" title="Time complexity">time complexity</a> is bounded above by a primitive recursive function of the input size.<a href="#cite_note-FOOTNOTEHartmanis1989-2">[2]</a> It is hence not particularly easy to devise a <a href="Computable_function" title="Computable function">computable function</a> that is not primitive recursive; some examples are shown in section <a href="#Limitations">§ Limitations</a> below.

The set of primitive recursive functions is known as <a href="PR_(complexity)" title="PR (complexity)">PR</a> in <a href="Computational_complexity_theory" title="Computational complexity theory">computational complexity theory</a>.

<div class="mw-heading mw-heading2"><h2 id="Definition">Definition</h2></div>

A primitive recursive function takes a fixed number of arguments, each a <a href="Natural_number" title="Natural number">natural number</a> (nonnegative integer: {0, 1, 2, ...}), and returns a natural number. If it takes n arguments it is called n-<a href="Arity" title="Arity">ary</a>.

The basic primitive recursive functions are given by these <a href="Axiom" title="Axiom">axioms</a>:

<div><ol start="1"><li>Constant functions <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{n}^{k}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{n}^{k}}</annotation>

</semantics>

</math><img src="./9b088b67f00e4739e57c658ac7dd5913898013ac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.887ex; height:2.843ex;" alt="{\displaystyle C_{n}^{k}}" loading="lazy">: For each natural number <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy"> and every <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle k}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k}</annotation>

</semantics>

</math><img src="./c3c9a2c7b599b37105512c5d570edc034056dd40.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.211ex; height:2.176ex;" alt="{\displaystyle k}" loading="lazy">, the k-ary constant function, defined by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{n}^{k}(x_{1},\ldots ,x_{k})\ {\stackrel {\mathrm {def} }{=}}\ n}">

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mover>

</mrow>

</mrow>

</mover>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{n}^{k}(x_{1},\ldots ,x_{k})\ {\stackrel {\mathrm {def} }{=}}\ n}</annotation>

</semantics>

</math><img src="./c37184786012801a8d6a2123ad2e2af0bd9f5e54.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.488ex; height:3.843ex;" alt="{\displaystyle C_{n}^{k}(x_{1},\ldots ,x_{k})\ {\stackrel {\mathrm {def} }{=}}\ n}" loading="lazy">, is primitive recursive.</li><li>Successor function: The 1-ary successor function S, which returns the successor of its argument (see <a href="Peano_postulates" class="mw-redirect" title="Peano postulates">Peano postulates</a>), that is, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S(x)\ {\stackrel {\mathrm {def} }{=}}\ x+1}">

<mover>

</mrow>

</mrow>

</mover>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S(x)\ {\stackrel {\mathrm {def} }{=}}\ x+1}</annotation>

</semantics>

</math><img src="./1e6968a6149cf34f1744866e54111df6e88b39ad.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.388ex; height:3.843ex;" alt="{\displaystyle S(x)\ {\stackrel {\mathrm {def} }{=}}\ x+1}" loading="lazy">, is primitive recursive.</li><li>Projection functions <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P_{i}^{k}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P_{i}^{k}}</annotation>

</semantics>

</math><img src="./361d716d235d131f6d22554b9b4797923c3be3c5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.91ex; height:3.176ex;" alt="{\displaystyle P_{i}^{k}}" loading="lazy">: For all natural numbers <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i,k}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i,k}</annotation>

</semantics>

</math><img src="./c3885ba48fa465d00556c235647088efbd248c26.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.048ex; height:2.509ex;" alt="{\displaystyle i,k}" loading="lazy"> such that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 1\leq i\leq k}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 1\leq i\leq k}</annotation>

</semantics>

</math><img src="./83de74da899efbafa01ec98ebf478e9ce5679fc6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:9.373ex; height:2.343ex;" alt="{\displaystyle 1\leq i\leq k}" loading="lazy">, the k-ary function defined by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P_{i}^{k}(x_{1},\ldots ,x_{k})\ {\stackrel {\mathrm {def} }{=}}\ x_{i}}">

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mover>

</mrow>

</mrow>

</mover>

</mrow>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P_{i}^{k}(x_{1},\ldots ,x_{k})\ {\stackrel {\mathrm {def} }{=}}\ x_{i}}</annotation>

</semantics>

</math><img src="./6c61983e4beadbeeec6813f4cc01b6c2d92da367.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:20.246ex; height:4.009ex;" alt="{\displaystyle P_{i}^{k}(x_{1},\ldots ,x_{k})\ {\stackrel {\mathrm {def} }{=}}\ x_{i}}" loading="lazy"> is primitive recursive.</li></ol></div>

More complex primitive recursive functions can be obtained by applying the <a href="Operation_(mathematics)" title="Operation (mathematics)">operations</a> given by these axioms:

<div><ol start="4"><li>Composition operator <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \circ \,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \circ \,}</annotation>

</semantics>

</math><img src="./307536c9e69fa4336e75b99e39243bd02d80f5fd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.171ex; width:1.55ex; height:1.509ex;" alt="{\displaystyle \circ \,}" loading="lazy"> (also called the substitution operator): Given an m-ary function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h(x_{1},\ldots ,x_{m})\,}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h(x_{1},\ldots ,x_{m})\,}</annotation>

</semantics>

</math><img src="./365d0558c7c9c47e4eaa64438fe7f22c5f1f659e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.102ex; height:2.843ex;" alt="{\displaystyle h(x_{1},\ldots ,x_{m})\,}" loading="lazy"> and m k-ary functions <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g_{1}(x_{1},\ldots ,x_{k}),\ldots ,g_{m}(x_{1},\ldots ,x_{k})}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g_{1}(x_{1},\ldots ,x_{k}),\ldots ,g_{m}(x_{1},\ldots ,x_{k})}</annotation>

</semantics>

</math><img src="./d08afd5fedccb61860b7a7eadc6e41dd3bf6f5fb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.705ex; height:2.843ex;" alt="{\displaystyle g_{1}(x_{1},\ldots ,x_{k}),\ldots ,g_{m}(x_{1},\ldots ,x_{k})}" loading="lazy">: <math display="block" xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h\circ (g_{1},\ldots ,g_{m})\ {\stackrel {\mathrm {def} }{=}}\ f,\quad {\text{where}}\quad f(x_{1},\ldots ,x_{k})=h(g_{1}(x_{1},\ldots ,x_{k}),\ldots ,g_{m}(x_{1},\ldots ,x_{k})).}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mover>

</mrow>

</mrow>

</mover>

</mrow>

<mtext>where</mtext>

</mrow>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h\circ (g_{1},\ldots ,g_{m})\ {\stackrel {\mathrm {def} }{=}}\ f,\quad {\text{where}}\quad f(x_{1},\ldots ,x_{k})=h(g_{1}(x_{1},\ldots ,x_{k}),\ldots ,g_{m}(x_{1},\ldots ,x_{k})).}</annotation>

</semantics>

</math> For <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle m=1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle m=1}</annotation>

</semantics>

</math><img src="./b6100c5ebd48c6fd848709f2be624465203eb173.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.301ex; height:2.176ex;" alt="{\displaystyle m=1}" loading="lazy">, the ordinary <a href="Function_composition" title="Function composition">function composition</a> <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h\circ g_{1}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h\circ g_{1}}</annotation>

</semantics>

</math><img src="./bb4f759686bbd17331623bf5c5efb2b76188632e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.697ex; height:2.509ex;" alt="{\displaystyle h\circ g_{1}}" loading="lazy"> is obtained.</li><li>Primitive recursion operator <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \rho }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \rho }</annotation>

</semantics>

</math><img src="./1f7d439671d1289b6a816e6af7a304be40608d64.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:1.202ex; height:2.176ex;" alt="{\displaystyle \rho }" loading="lazy">: Given the k-ary function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g(x_{1},\ldots ,x_{k})\,}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g(x_{1},\ldots ,x_{k})\,}</annotation>

</semantics>

</math><img src="./0a070f67fcfdb007cc3bb2afa075fc86722876da.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.293ex; height:2.843ex;" alt="{\displaystyle g(x_{1},\ldots ,x_{k})\,}" loading="lazy"> and the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (k+2)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (k+2)}</annotation>

</semantics>

</math><img src="./c8af963731a6f9664ee81b251d48c96d92f5582a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.023ex; height:2.843ex;" alt="{\displaystyle (k+2)}" loading="lazy">-ary function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h(y,z,x_{1},\ldots ,x_{k})\,}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h(y,z,x_{1},\ldots ,x_{k})\,}</annotation>

</semantics>

</math><img src="./f7854e20a91c28109d5fcc4c6ba29477f01858d1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.827ex; height:2.843ex;" alt="{\displaystyle h(y,z,x_{1},\ldots ,x_{k})\,}" loading="lazy">:

<mtr>

<mtd>

</mtd>

<mtd>

<mover>

</mrow>

</mrow>

</mover>

</mrow>

<mtext>where the </mtext>

</mrow>

<mtext>-ary function </mtext>

</mrow>

<mtext> is defined by</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

<mrow>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

<msup>

</msup>

<msup>

</msup>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mrow>

<msup>

</msup>

</mrow>

<msup>

</msup>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\rho (g,h)&\ {\stackrel {\mathrm {def} }{=}}\ f,\quad {\text{where the }}(k+1){\text{-ary function }}f{\text{ is defined by}}\\f(y,x_{1},\dots ,x_{k})&={\begin{cases}g(x_{1},\dots ,x_{k})&{\text{if }}y=0\\h(y',f(y',x_{1},\dots ,x_{k}),x_{1},\dots ,x_{k})&{\text{if }}y=S(y'){\text{ for a }}y'\in \mathbb {N} \\\end{cases}}\end{aligned}}}</annotation>

</semantics>

</math></dd></dl>

Interpretation:

The function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f}</annotation>

</semantics>

</math><img src="./132e57acb643253e7810ee9702d9581f159a1c61.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}" loading="lazy"> acts as a <a href="For_loop" title="For loop">for-loop</a> from <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 0}</annotation>

</semantics>

</math><img src="./2aae8864a3c1fec9585261791a809ddec1489950.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}" loading="lazy"> up to the value of its first argument. The rest of the arguments for <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f}</annotation>

</semantics>

</math><img src="./132e57acb643253e7810ee9702d9581f159a1c61.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}" loading="lazy">, denoted here with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1},\ldots ,x_{k}}">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x_{1},\ldots ,x_{k}}</annotation>

</semantics>

</math><img src="./00a6511886c686290cc57b23ab22f45fda9e1c12.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:9.981ex; height:2.009ex;" alt="{\displaystyle x_{1},\ldots ,x_{k}}" loading="lazy">, are a set of initial conditions for the for-loop which may be used by it during calculations but which are immutable by it. The functions <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g}</annotation>

</semantics>

</math><img src="./d3556280e66fe2c0d0140df20935a6f057381d77.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.116ex; height:2.009ex;" alt="{\displaystyle g}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"> on the right-hand side of the equations that define <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f}</annotation>

</semantics>

</math><img src="./132e57acb643253e7810ee9702d9581f159a1c61.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}" loading="lazy"> represent the body of the loop, which performs calculations. The function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g}</annotation>

</semantics>

</math><img src="./d3556280e66fe2c0d0140df20935a6f057381d77.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.116ex; height:2.009ex;" alt="{\displaystyle g}" loading="lazy"> is used only once to perform initial calculations. Calculations for subsequent steps of the loop are performed by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy">. The first parameter of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"> is fed the "current" value of the for-loop's index. The second parameter of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"> is fed the result of the for-loop's previous calculations, from previous steps. The rest of the parameters for <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"> are those immutable initial conditions for the for-loop mentioned earlier. They may be used by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"> to perform calculations but they will not themselves be altered by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy">.</li></ol></div>

The primitive recursive functions are the basic functions and those obtained from the basic functions by applying these operations a finite number of times.

<div class="mw-heading mw-heading3"><h3 id="Primitive-recursiveness_of_vector-valued_functions">Primitive-recursiveness of vector-valued functions</h3></div>

A (vector-valued) function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f:\mathbb {N} ^{m}\to \mathbb {N} ^{n}}">

<msup>

</mrow>

</mrow>

</msup>

<msup>

</mrow>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f:\mathbb {N} ^{m}\to \mathbb {N} ^{n}}</annotation>

</semantics>

</math><img src="./951fbaafd50eda65114a31d784ac920548a0fc48.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.079ex; height:2.676ex;" alt="{\displaystyle f:\mathbb {N} ^{m}\to \mathbb {N} ^{n}}" loading="lazy"> is primitive recursive if it can be written as

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f(x_{1},\dots ,x_{m})=(f_{1}(x_{1},\dots ,x_{m}),\dots ,f_{n}(x_{1},\dots ,x_{m}))}</annotation>

</semantics>

</math><img src="./9bb1d5492eda10debe374f751df2253f9e905023.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:53.044ex; height:2.843ex;" alt="{\displaystyle f(x_{1},\dots ,x_{m})=(f_{1}(x_{1},\dots ,x_{m}),\dots ,f_{n}(x_{1},\dots ,x_{m}))}" loading="lazy"></dd></dl>

where each component <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f_{i}:\mathbb {N} ^{m}\to \mathbb {N} }">

<msub>

</mrow>

</msub>

<msup>

</mrow>

</mrow>

</msup>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f_{i}:\mathbb {N} ^{m}\to \mathbb {N} }</annotation>

</semantics>

</math><img src="./6c90f2d7637bdbbf6ec2f50d369575a15ed381bc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:12.521ex; height:2.676ex;" alt="{\displaystyle f_{i}:\mathbb {N} ^{m}\to \mathbb {N} }" loading="lazy"> is a (scalar-valued) primitive recursive function.<a href="#cite_note-3">[3]</a>

<div class="mw-heading mw-heading2"><h2 id="Examples">Examples</h2></div>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{0}^{1}}</annotation>

</semantics>

</math><img src="./d9f73107cfc3d7b29e540b3b7b6c5d070b56faf0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.852ex; height:3.176ex;" alt="{\displaystyle C_{0}^{1}}" loading="lazy"> is a 1-ary function which returns <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 0}</annotation>

</semantics>

</math><img src="./2aae8864a3c1fec9585261791a809ddec1489950.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}" loading="lazy"> for every input: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{0}^{1}(x)=0}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{0}^{1}(x)=0}</annotation>

</semantics>

</math><img src="./70f2b2de034a6d0ad3674a805148b0c3407de4ff.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:10.252ex; height:3.176ex;" alt="{\displaystyle C_{0}^{1}(x)=0}" loading="lazy">.</li><li><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{1}^{1}}</annotation>

</semantics>

</math><img src="./19ff89472a2f5860873c8ed7e2c325e0127af9c6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.852ex; height:3.176ex;" alt="{\displaystyle C_{1}^{1}}" loading="lazy"> is a 1-ary function which returns <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 1}</annotation>

</semantics>

</math><img src="./92d98b82a3778f043108d4e20960a9193df57cbf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 1}" loading="lazy"> for every input: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}^{1}(x)=1}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{1}^{1}(x)=1}</annotation>

</semantics>

</math><img src="./5d1eaa922c1a06cecfb0d90ebaecb6d66868f8d6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:10.252ex; height:3.176ex;" alt="{\displaystyle C_{1}^{1}(x)=1}" loading="lazy">.</li><li><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{3}^{0}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{3}^{0}}</annotation>

</semantics>

</math><img src="./4ba04f077557a4244b523d33ad7ffeb9ed911444.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.852ex; height:3.176ex;" alt="{\displaystyle C_{3}^{0}}" loading="lazy"> is a 0-ary function, i.e. a constant: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{3}^{0}=3}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{3}^{0}=3}</annotation>

</semantics>

</math><img src="./065a00293795724443500bca36da88d57d0cbc59.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:7.113ex; height:3.176ex;" alt="{\displaystyle C_{3}^{0}=3}" loading="lazy">.</li><li><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P_{1}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P_{1}^{1}}</annotation>

</semantics>

</math><img src="./cf986b1a355d299b662f53917ebff839f24c38fd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.876ex; height:3.176ex;" alt="{\displaystyle P_{1}^{1}}" loading="lazy"> is the identity function on the natural numbers: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P_{1}^{1}(x)=x}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P_{1}^{1}(x)=x}</annotation>

</semantics>

</math><img src="./709354ab58433129309ead618819747c52e0ac80.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:10.443ex; height:3.176ex;" alt="{\displaystyle P_{1}^{1}(x)=x}" loading="lazy">.</li><li><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P_{1}^{2}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P_{1}^{2}}</annotation>

</semantics>

</math><img src="./bd897d977403f9d802ce876f067f84a5959ad8ff.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.876ex; height:3.176ex;" alt="{\displaystyle P_{1}^{2}}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P_{2}^{2}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P_{2}^{2}}</annotation>

</semantics>

</math><img src="./6bd701a007b58e3547ee212141fba8cdf4994256.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.876ex; height:3.176ex;" alt="{\displaystyle P_{2}^{2}}" loading="lazy"> is the left and right projection on natural number pairs, respectively: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P_{1}^{2}(x,y)=x}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P_{1}^{2}(x,y)=x}</annotation>

</semantics>

</math><img src="./133f9cf4088eec019ee2515470e9c086dcbe5de9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:12.632ex; height:3.176ex;" alt="{\displaystyle P_{1}^{2}(x,y)=x}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle P_{2}^{2}(x,y)=y}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle P_{2}^{2}(x,y)=y}</annotation>

</semantics>

</math><img src="./500493659d5cf4628765cdf6be9b04140502b8ac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:12.458ex; height:3.176ex;" alt="{\displaystyle P_{2}^{2}(x,y)=y}" loading="lazy">.</li><li><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\circ S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S\circ S}</annotation>

</semantics>

</math><img src="./ce4de5e9fb4ac348e94f52ab7a8ff07dd1539b8a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.193ex; height:2.176ex;" alt="{\displaystyle S\circ S}" loading="lazy"> is a 1-ary function that adds 2 to its input, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (S\circ S)(x)=x+2}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (S\circ S)(x)=x+2}</annotation>

</semantics>

</math><img src="./db896b4ed0755ce57dbebb8473b1deda53e83d08.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.572ex; height:2.843ex;" alt="{\displaystyle (S\circ S)(x)=x+2}" loading="lazy">.</li><li><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\circ C_{0}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S\circ C_{0}^{1}}</annotation>

</semantics>

</math><img src="./f84a6549323e3daa820e437c76f635d7f248d896.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:6.546ex; height:3.176ex;" alt="{\displaystyle S\circ C_{0}^{1}}" loading="lazy"> is a 1-ary function which returns 1 for every input: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (S\circ C_{0}^{1})(x)=S(C_{0}^{1}(x))=S(0)=1}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (S\circ C_{0}^{1})(x)=S(C_{0}^{1}(x))=S(0)=1}</annotation>

</semantics>

</math><img src="./d54c4fc5e62998cc9d6364aef5bed6f56336ffcc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:35.723ex; height:3.176ex;" alt="{\displaystyle (S\circ C_{0}^{1})(x)=S(C_{0}^{1}(x))=S(0)=1}" loading="lazy">. That is, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\circ C_{0}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S\circ C_{0}^{1}}</annotation>

</semantics>

</math><img src="./f84a6549323e3daa820e437c76f635d7f248d896.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:6.546ex; height:3.176ex;" alt="{\displaystyle S\circ C_{0}^{1}}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{1}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{1}^{1}}</annotation>

</semantics>

</math><img src="./19ff89472a2f5860873c8ed7e2c325e0127af9c6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.852ex; height:3.176ex;" alt="{\displaystyle C_{1}^{1}}" loading="lazy"> are the same function: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\circ C_{0}^{1}=C_{1}^{1}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S\circ C_{0}^{1}=C_{1}^{1}}</annotation>

</semantics>

</math><img src="./664b3ebca2a05c0016664a661a0355393c471093.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:12.496ex; height:3.176ex;" alt="{\displaystyle S\circ C_{0}^{1}=C_{1}^{1}}" loading="lazy">. In a similar way, every <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{n}^{k}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{n}^{k}}</annotation>

</semantics>

</math><img src="./9b088b67f00e4739e57c658ac7dd5913898013ac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.887ex; height:2.843ex;" alt="{\displaystyle C_{n}^{k}}" loading="lazy"> can be expressed as a composition of appropriately many <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S}</annotation>

</semantics>

</math><img src="./4611d85173cd3b508e67077d4a1252c9c05abca2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{0}^{k}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{0}^{k}}</annotation>

</semantics>

</math><img src="./aa83360fbe63e63b0358e32e5743253712b59d32.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.887ex; height:3.176ex;" alt="{\displaystyle C_{0}^{k}}" loading="lazy">. Moreover, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{0}^{k}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{0}^{k}}</annotation>

</semantics>

</math><img src="./aa83360fbe63e63b0358e32e5743253712b59d32.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.887ex; height:3.176ex;" alt="{\displaystyle C_{0}^{k}}" loading="lazy"> equals <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{0}^{1}\circ P_{1}^{k}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{0}^{1}\circ P_{1}^{k}}</annotation>

</semantics>

</math><img src="./3a87bdaa04962d39f997c97769cfdc008869776d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:7.957ex; height:3.176ex;" alt="{\displaystyle C_{0}^{1}\circ P_{1}^{k}}" loading="lazy">, since <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{0}^{k}(x_{1},\ldots ,x_{k})=0=C_{0}^{1}(x_{1})=C_{0}^{1}(P_{1}^{k}(x_{1},\ldots ,x_{k}))=(C_{0}^{1}\circ P_{1}^{k})(x_{1},\ldots ,x_{k})}">

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{0}^{k}(x_{1},\ldots ,x_{k})=0=C_{0}^{1}(x_{1})=C_{0}^{1}(P_{1}^{k}(x_{1},\ldots ,x_{k}))=(C_{0}^{1}\circ P_{1}^{k})(x_{1},\ldots ,x_{k})}</annotation>

</semantics>

</math><img src="./e09ba19f0578b664b4de20672d6996071d85adf8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:76.195ex; height:3.176ex;" alt="{\displaystyle C_{0}^{k}(x_{1},\ldots ,x_{k})=0=C_{0}^{1}(x_{1})=C_{0}^{1}(P_{1}^{k}(x_{1},\ldots ,x_{k}))=(C_{0}^{1}\circ P_{1}^{k})(x_{1},\ldots ,x_{k})}" loading="lazy">. For these reasons, some authors<a href="#cite_note-4">[4]</a> define <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{n}^{k}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{n}^{k}}</annotation>

</semantics>

</math><img src="./9b088b67f00e4739e57c658ac7dd5913898013ac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.887ex; height:2.843ex;" alt="{\displaystyle C_{n}^{k}}" loading="lazy"> only for <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n=0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n=0}</annotation>

</semantics>

</math><img src="./26819344e55f5e671c76c07c18eb4291fcec85ae.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.656ex; height:2.176ex;" alt="{\displaystyle n=0}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle k=1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k=1}</annotation>

</semantics>

</math><img src="./6c035ffa69b5bca8bf2d16c3da3aaad79a8bcbfa.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.472ex; height:2.176ex;" alt="{\displaystyle k=1}" loading="lazy">.</li></ul></div>

<div class="mw-heading mw-heading3"><h3 id="Addition">Addition</h3></div>

A definition of the 2-ary function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Add}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Add}</annotation>

</semantics>

</math><img src="./8123fd1136a666d741f090c10185d254d88df8e7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.175ex; height:2.176ex;" alt="{\displaystyle Add}" loading="lazy">, to compute the sum of its arguments, can be obtained using the primitive recursion operator <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \rho }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \rho }</annotation>

</semantics>

</math><img src="./1f7d439671d1289b6a816e6af7a304be40608d64.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:1.202ex; height:2.176ex;" alt="{\displaystyle \rho }" loading="lazy">. To this end, the well-known equations

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{rcll}0+y&=&y&{\text{ and}}\\S(x)+y&=&S(x+y)&.\\\end{array}}}</annotation>

</semantics>

</math><img src="./f44eb64b90d4b117d36f6e3c28ce5ac73dcae7d4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:31.124ex; height:6.176ex;" alt="{\displaystyle {\begin{array}{rcll}0+y&=&y&{\text{ and}}\\S(x)+y&=&S(x+y)&.\\\end{array}}}" loading="lazy"></dd></dl>

are "rephrased in primitive recursive function terminology": In the definition of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \rho (g,h)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \rho (g,h)}</annotation>

</semantics>

</math><img src="./415c8a701049b2fa80d00659d846f5012f91073a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.5ex; height:2.843ex;" alt="{\displaystyle \rho (g,h)}" loading="lazy">, the first equation suggests to choose <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g=P_{1}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g=P_{1}^{1}}</annotation>

</semantics>

</math><img src="./cbfd76dea051eb2bdef3362d67bba463bf9c5d5d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:7.09ex; height:3.176ex;" alt="{\displaystyle g=P_{1}^{1}}" loading="lazy"> to obtain <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Add(0,y)=g(y)=y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Add(0,y)=g(y)=y}</annotation>

</semantics>

</math><img src="./a35752e62d307f3c757b61b0bb602966fb8ef1fe.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.769ex; height:2.843ex;" alt="{\displaystyle Add(0,y)=g(y)=y}" loading="lazy">; the second equation suggests to choose <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h=S\circ P_{2}^{3}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h=S\circ P_{2}^{3}}</annotation>

</semantics>

</math><img src="./7d694158c20ad11cd6f239a7bfc2aec42ef053f9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:11.007ex; height:3.176ex;" alt="{\displaystyle h=S\circ P_{2}^{3}}" loading="lazy"> to obtain <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Add(S(x),y)=h(x,Add(x,y),y)=(S\circ P_{2}^{3})(x,Add(x,y),y)=S(Add(x,y))}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Add(S(x),y)=h(x,Add(x,y),y)=(S\circ P_{2}^{3})(x,Add(x,y),y)=S(Add(x,y))}</annotation>

</semantics>

</math><img src="./4e8e8a0108a6cda837c762f42776c4945262c145.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:76.368ex; height:3.176ex;" alt="{\displaystyle Add(S(x),y)=h(x,Add(x,y),y)=(S\circ P_{2}^{3})(x,Add(x,y),y)=S(Add(x,y))}" loading="lazy">. Therefore, the addition function can be defined as <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Add=\rho (P_{1}^{1},S\circ P_{2}^{3})}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Add=\rho (P_{1}^{1},S\circ P_{2}^{3})}</annotation>

</semantics>

</math><img src="./c90a3ac70eb3a50bb02046a775816d9ce7133dbe.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:20.764ex; height:3.176ex;" alt="{\displaystyle Add=\rho (P_{1}^{1},S\circ P_{2}^{3})}" loading="lazy">. As a computation example,

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lll}&Add(1,7)\\=&\rho (P_{1}^{1},S\circ P_{2}^{3})\;(S(0),7)&{\text{ by Def. }}Add,S\\=&(S\circ P_{2}^{3})(0,Add(0,7),7)&{\text{ by case }}\rho (g,h)\;(S(...),...)\\=&S(Add(0,7))&{\text{ by Def. }}\circ ,P_{2}^{3}\\=&S(\;\rho (P_{1}^{1},S\circ P_{2}^{3})\;(0,7)\;)&{\text{ by Def. }}Add\\=&S(P_{1}^{1}(7))&{\text{ by case }}\rho (g,h)\;(0,...)\\=&S(7)&{\text{ by Def. }}P_{1}^{1}\\=&8&{\text{ by Def. }}S.\\\end{array}}}</annotation>

</semantics>

</math><img src="./d0e2f76d98cbe4d77277264533f14ba1fc2e88f4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -12.964ex; margin-bottom: -0.207ex; width:59.035ex; height:27.509ex;" alt="{\displaystyle {\begin{array}{lll}&Add(1,7)\\=&\rho (P_{1}^{1},S\circ P_{2}^{3})\;(S(0),7)&{\text{ by Def. }}Add,S\\=&(S\circ P_{2}^{3})(0,Add(0,7),7)&{\text{ by case }}\rho (g,h)\;(S(...),...)\\=&S(Add(0,7))&{\text{ by Def. }}\circ ,P_{2}^{3}\\=&S(\;\rho (P_{1}^{1},S\circ P_{2}^{3})\;(0,7)\;)&{\text{ by Def. }}Add\\=&S(P_{1}^{1}(7))&{\text{ by case }}\rho (g,h)\;(0,...)\\=&S(7)&{\text{ by Def. }}P_{1}^{1}\\=&8&{\text{ by Def. }}S.\\\end{array}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Doubling">Doubling</h3></div>

Given <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Add}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Add}</annotation>

</semantics>

</math><img src="./8123fd1136a666d741f090c10185d254d88df8e7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.175ex; height:2.176ex;" alt="{\displaystyle Add}" loading="lazy">, the 1-ary function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Add\circ (P_{1}^{1},P_{1}^{1})}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Add\circ (P_{1}^{1},P_{1}^{1})}</annotation>

</semantics>

</math><img src="./b9345d0dcbc7e5bdc72dfb442069d7ffe5bcb934.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:14.964ex; height:3.176ex;" alt="{\displaystyle Add\circ (P_{1}^{1},P_{1}^{1})}" loading="lazy"> doubles its argument, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (Add\circ (P_{1}^{1},P_{1}^{1}))(x)=Add(x,x)=x+x}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (Add\circ (P_{1}^{1},P_{1}^{1}))(x)=Add(x,x)=x+x}</annotation>

</semantics>

</math><img src="./e430c8457e5e010d6e6b3c2c520062ebf535dc31.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:41.287ex; height:3.176ex;" alt="{\displaystyle (Add\circ (P_{1}^{1},P_{1}^{1}))(x)=Add(x,x)=x+x}" loading="lazy">.

<div class="mw-heading mw-heading3"><h3 id="Multiplication">Multiplication</h3></div>

In a similar way as addition, multiplication can be defined by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Mul=\rho (C_{0}^{1},Add\circ (P_{2}^{3},P_{3}^{3}))}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Mul=\rho (C_{0}^{1},Add\circ (P_{2}^{3},P_{3}^{3}))}</annotation>

</semantics>

</math><img src="./abf2746ec392c9baaa9c0f2555214455baae6103.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:29.425ex; height:3.176ex;" alt="{\displaystyle Mul=\rho (C_{0}^{1},Add\circ (P_{2}^{3},P_{3}^{3}))}" loading="lazy">. This reproduces the well-known multiplication equations:

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lll}&Mul(0,y)\\=&\rho (C_{0}^{1},Add\circ (P_{2}^{3},P_{3}^{3}))\;(0,y)&{\text{ by Def. }}Mul\\=&C_{0}^{1}(y)&{\text{ by case }}\rho (g,h)\;(0,...)\\=&0&{\text{ by Def. }}C_{0}^{1}.\\\end{array}}}</annotation>

</semantics>

</math><img src="./6bba8f7fb4ba0698d6ed10c43e1edf2245bd9d6d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -6.338ex; width:57.531ex; height:13.843ex;" alt="{\displaystyle {\begin{array}{lll}&Mul(0,y)\\=&\rho (C_{0}^{1},Add\circ (P_{2}^{3},P_{3}^{3}))\;(0,y)&{\text{ by Def. }}Mul\\=&C_{0}^{1}(y)&{\text{ by case }}\rho (g,h)\;(0,...)\\=&0&{\text{ by Def. }}C_{0}^{1}.\\\end{array}}}" loading="lazy"></dd></dl>

and

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

<mtext> by property of </mtext>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lll}&Mul(S(x),y)\\=&\rho (C_{0}^{1},Add\circ (P_{2}^{3},P_{3}^{3}))\;(S(x),y)&{\text{ by Def. }}Mul\\=&(Add\circ (P_{2}^{3},P_{3}^{3}))\;(x,Mul(x,y),y)&{\text{ by case }}\rho (g,h)\;(S(...),...)\\=&Add(Mul(x,y),y)&{\text{ by Def. }}\circ ,P_{2}^{3},P_{3}^{3}\\=&Mul(x,y)+y&{\text{ by property of }}Add.\\\end{array}}}</annotation>

</semantics>

</math><img src="./014db37df652711a2433f8d55052e27b5c9b144e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -7.741ex; margin-bottom: -0.264ex; width:68.686ex; height:17.176ex;" alt="{\displaystyle {\begin{array}{lll}&Mul(S(x),y)\\=&\rho (C_{0}^{1},Add\circ (P_{2}^{3},P_{3}^{3}))\;(S(x),y)&{\text{ by Def. }}Mul\\=&(Add\circ (P_{2}^{3},P_{3}^{3}))\;(x,Mul(x,y),y)&{\text{ by case }}\rho (g,h)\;(S(...),...)\\=&Add(Mul(x,y),y)&{\text{ by Def. }}\circ ,P_{2}^{3},P_{3}^{3}\\=&Mul(x,y)+y&{\text{ by property of }}Add.\\\end{array}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Predecessor">Predecessor</h3></div>

The predecessor function acts as the "opposite" of the successor function and is recursively defined by the rules <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Pred(0)=0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred(0)=0}</annotation>

</semantics>

</math><img src="./8a0b709e9776bd08e29ca836ec9635e3b47f99a9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.326ex; height:2.843ex;" alt="{\displaystyle Pred(0)=0}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Pred(S(n))=n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred(S(n))=n}</annotation>

</semantics>

</math><img src="./f4dfbc27d5dce3374fe5b8d9a372608b8af09b4e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.099ex; height:2.843ex;" alt="{\displaystyle Pred(S(n))=n}" loading="lazy">. A primitive recursive definition is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Pred=\rho (C_{0}^{0},P_{1}^{2})}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred=\rho (C_{0}^{0},P_{1}^{2})}</annotation>

</semantics>

</math><img src="./0cac8717442d8beee4186d5b9241928d5cd96e7f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:17.965ex; height:3.176ex;" alt="{\displaystyle Pred=\rho (C_{0}^{0},P_{1}^{2})}" loading="lazy">. As a computation example,

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lll}&Pred(8)\\=&\rho (C_{0}^{0},P_{1}^{2})\;(S(7))&{\text{ by Def. }}Pred,S\\=&P_{1}^{2}(7,Pred(7))&{\text{ by case }}\rho (g,h)\;(S(...),...)\\=&7&{\text{ by Def. }}P_{1}^{2}.\\\end{array}}}</annotation>

</semantics>

</math><img src="./49728351a759a56ae1c1ddb806584731198b9b2f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -6.171ex; width:51.809ex; height:13.509ex;" alt="{\displaystyle {\begin{array}{lll}&Pred(8)\\=&\rho (C_{0}^{0},P_{1}^{2})\;(S(7))&{\text{ by Def. }}Pred,S\\=&P_{1}^{2}(7,Pred(7))&{\text{ by case }}\rho (g,h)\;(S(...),...)\\=&7&{\text{ by Def. }}P_{1}^{2}.\\\end{array}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Truncated_subtraction">Truncated subtraction</h3></div>

The limited subtraction function (also called "<a href="Monus" title="Monus">monus</a>", and denoted "<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \mathbin {\dot {-}} }">

<mover>

</mover>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \mathbin {\dot {-}} }</annotation>

</semantics>

</math><img src="./4c2e6225edc14b7298f08b5e047b05b06b52616d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:1.808ex; height:2.676ex;" alt="{\displaystyle \mathbin {\dot {-}} }" loading="lazy">") is definable from the predecessor function. It satisfies the equations

<mtr>

<mtd>

<mover>

</mover>

</mrow>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

<mover>

</mover>

</mrow>

</mtd>

<mtd>

</mtd>

<mtd>

<mover>

</mover>

</mrow>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{rcll}y\mathbin {\dot {-}} 0&=&y&{\text{and}}\\y\mathbin {\dot {-}} S(x)&=&Pred(y\mathbin {\dot {-}} x)&.\\\end{array}}}</annotation>

</semantics>

</math><img src="./c3b818769701802c8ee5cd00bb472c2efb841843.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:34.137ex; height:6.176ex;" alt="{\displaystyle {\begin{array}{rcll}y\mathbin {\dot {-}} 0&=&y&{\text{and}}\\y\mathbin {\dot {-}} S(x)&=&Pred(y\mathbin {\dot {-}} x)&.\\\end{array}}}" loading="lazy"></dd></dl>

Since the recursion runs over the second argument, we begin with a primitive recursive definition of the reversed subtraction, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle RSub(y,x)=x\mathbin {\dot {-}} y}">

<mover>

</mover>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle RSub(y,x)=x\mathbin {\dot {-}} y}</annotation>

</semantics>

</math><img src="./9fd5b893ab8d2a00d9ec42bbf318b7fe26c8df09.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.343ex; height:3.009ex;" alt="{\displaystyle RSub(y,x)=x\mathbin {\dot {-}} y}" loading="lazy">. Its recursion then runs over the first argument, so its primitive recursive definition can be obtained, similar to addition, as <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle RSub=\rho (P_{1}^{1},Pred\circ P_{2}^{3})}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle RSub=\rho (P_{1}^{1},Pred\circ P_{2}^{3})}</annotation>

</semantics>

</math><img src="./cebec2a09c7a0ceca0136decb1fe1e40a73531cb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:25.774ex; height:3.176ex;" alt="{\displaystyle RSub=\rho (P_{1}^{1},Pred\circ P_{2}^{3})}" loading="lazy">. To get rid of the reversed argument order, then define <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Sub=RSub\circ (P_{2}^{2},P_{1}^{2})}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Sub=RSub\circ (P_{2}^{2},P_{1}^{2})}</annotation>

</semantics>

</math><img src="./5a9e6afedd0066a0dbe66f22402b14fc7db3f259.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:23.305ex; height:3.176ex;" alt="{\displaystyle Sub=RSub\circ (P_{2}^{2},P_{1}^{2})}" loading="lazy">. As a computation example,

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

<mtext> by property of </mtext>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lll}&Sub(8,1)\\=&(RSub\circ (P_{2}^{2},P_{1}^{2}))\;(8,1)&{\text{ by Def. }}Sub\\=&RSub(1,8)&{\text{ by Def. }}\circ ,P_{2}^{2},P_{1}^{2}\\=&\rho (P_{1}^{1},Pred\circ P_{2}^{3})\;(S(0),8)&{\text{ by Def. }}RSub,S\\=&(Pred\circ P_{2}^{3})\;(0,RSub(0,8),8)&{\text{ by case }}\rho (g,h)\;(S(...),...)\\=&Pred(RSub(0,8))&{\text{ by Def. }}\circ ,P_{2}^{3}\\=&Pred(\;\rho (P_{1}^{1},Pred\circ P_{2}^{3})\;(0,8)\;)&{\text{ by Def. }}RSub\\=&Pred(P_{1}^{1}(8))&{\text{ by case }}\rho (g,h)\;(0,...)\\=&Pred(8)&{\text{ by Def. }}P_{1}^{1}\\=&7&{\text{ by property of }}Pred.\\\end{array}}}</annotation>

</semantics>

</math><img src="./90bf6400712c7487eaefb06b6894eda339ddf9dc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -16.505ex; margin-bottom: -0.333ex; width:66.202ex; height:34.843ex;" alt="{\displaystyle {\begin{array}{lll}&Sub(8,1)\\=&(RSub\circ (P_{2}^{2},P_{1}^{2}))\;(8,1)&{\text{ by Def. }}Sub\\=&RSub(1,8)&{\text{ by Def. }}\circ ,P_{2}^{2},P_{1}^{2}\\=&\rho (P_{1}^{1},Pred\circ P_{2}^{3})\;(S(0),8)&{\text{ by Def. }}RSub,S\\=&(Pred\circ P_{2}^{3})\;(0,RSub(0,8),8)&{\text{ by case }}\rho (g,h)\;(S(...),...)\\=&Pred(RSub(0,8))&{\text{ by Def. }}\circ ,P_{2}^{3}\\=&Pred(\;\rho (P_{1}^{1},Pred\circ P_{2}^{3})\;(0,8)\;)&{\text{ by Def. }}RSub\\=&Pred(P_{1}^{1}(8))&{\text{ by case }}\rho (g,h)\;(0,...)\\=&Pred(8)&{\text{ by Def. }}P_{1}^{1}\\=&7&{\text{ by property of }}Pred.\\\end{array}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Converting_predicates_to_numeric_functions">Converting predicates to numeric functions</h3></div>

In some settings it is natural to consider primitive recursive functions that take as inputs tuples that mix numbers with <a href="Truth_value" title="Truth value">truth values</a> (that is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy"> for true and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f}</annotation>

</semantics>

</math><img src="./132e57acb643253e7810ee9702d9581f159a1c61.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}" loading="lazy"> for false), or that produce truth values as outputs.<a href="#cite_note-FOOTNOTEKleene1974226–227-5">[5]</a> This can be accomplished by identifying the truth values with numbers in any fixed manner. For example, it is common to identify the truth value <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy"> with the number <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 1}</annotation>

</semantics>

</math><img src="./92d98b82a3778f043108d4e20960a9193df57cbf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 1}" loading="lazy"> and the truth value <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f}</annotation>

</semantics>

</math><img src="./132e57acb643253e7810ee9702d9581f159a1c61.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}" loading="lazy"> with the number <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 0}</annotation>

</semantics>

</math><img src="./2aae8864a3c1fec9585261791a809ddec1489950.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}" loading="lazy">. Once this identification has been made, the <a href="Indicator_function" title="Indicator function">characteristic function</a> of a set <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy">, which always returns <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 1}</annotation>

</semantics>

</math><img src="./92d98b82a3778f043108d4e20960a9193df57cbf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 1}" loading="lazy"> or <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 0}</annotation>

</semantics>

</math><img src="./2aae8864a3c1fec9585261791a809ddec1489950.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}" loading="lazy">, can be viewed as a predicate that tells whether a number is in the set <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A}</annotation>

</semantics>

</math><img src="./7daff47fa58cdfd29dc333def748ff5fa4c923e3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.743ex; height:2.176ex;" alt="{\displaystyle A}" loading="lazy">. Such an identification of predicates with numeric functions will be assumed for the remainder of this article.

<div class="mw-heading mw-heading3"><h3 id="Predicate_"Is_zero"">Predicate "Is zero"</h3></div>

As an example for a primitive recursive predicate, the 1-ary function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle IsZero}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle IsZero}</annotation>

</semantics>

</math><img src="./47c7f5ceeeccd9e25f794c483c9365c9d3e5e278.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.202ex; height:2.176ex;" alt="{\displaystyle IsZero}" loading="lazy"> shall be defined such that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle IsZero(x)=1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle IsZero(x)=1}</annotation>

</semantics>

</math><img src="./3d3d08a836c73ede55558aaa5fac3a0a4b616aa4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.602ex; height:2.843ex;" alt="{\displaystyle IsZero(x)=1}" loading="lazy"> if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x=0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x=0}</annotation>

</semantics>

</math><img src="./953917eaf52f2e1baad54c8c9e3d6f9bb3710cdc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.591ex; height:2.176ex;" alt="{\displaystyle x=0}" loading="lazy">, and

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle IsZero(x)=0}</annotation>

</semantics>

</math><img src="./b9917803c33264570352fa6ed2b5399106f4fdbd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.602ex; height:2.843ex;" alt="{\displaystyle IsZero(x)=0}" loading="lazy">, otherwise. This can be achieved by defining <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle IsZero=\rho (C_{1}^{0},C_{0}^{2})}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle IsZero=\rho (C_{1}^{0},C_{0}^{2})}</annotation>

</semantics>

</math><img src="./f72140195d7c6904776f3ec2581db8a45e3ca8b3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:20.05ex; height:3.176ex;" alt="{\displaystyle IsZero=\rho (C_{1}^{0},C_{0}^{2})}" loading="lazy">. Then, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle IsZero(0)=\rho (C_{1}^{0},C_{0}^{2})(0)=C_{1}^{0}()=1}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle IsZero(0)=\rho (C_{1}^{0},C_{0}^{2})(0)=C_{1}^{0}()=1}</annotation>

</semantics>

</math><img src="./efe6f3d99c7b8fefa962684b2e4f06147ca26ab7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:38.014ex; height:3.176ex;" alt="{\displaystyle IsZero(0)=\rho (C_{1}^{0},C_{0}^{2})(0)=C_{1}^{0}()=1}" loading="lazy"> and e.g. <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle IsZero(8)=\rho (C_{1}^{0},C_{0}^{2})(S(7))=C_{0}^{2}(7,IsZero(7))=0}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle IsZero(8)=\rho (C_{1}^{0},C_{0}^{2})(S(7))=C_{0}^{2}(7,IsZero(7))=0}</annotation>

</semantics>

</math><img src="./beb9b5c9c0c3f9437908ae4554943032875a3baa.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:53.693ex; height:3.176ex;" alt="{\displaystyle IsZero(8)=\rho (C_{1}^{0},C_{0}^{2})(S(7))=C_{0}^{2}(7,IsZero(7))=0}" loading="lazy">.

<div class="mw-heading mw-heading3"><h3 id="Predicate_"Less_or_equal"">Predicate "Less or equal"</h3></div>

Using the property <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq y\iff x\mathbin {\dot {-}} y=0}">

<mover>

</mover>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x\leq y\iff x\mathbin {\dot {-}} y=0}</annotation>

</semantics>

</math><img src="./682e790e731687de4ebac82103401abaa9e4403c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:22.067ex; height:2.843ex;" alt="{\displaystyle x\leq y\iff x\mathbin {\dot {-}} y=0}" loading="lazy">, the 2-ary function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Leq}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Leq}</annotation>

</semantics>

</math><img src="./a976a2a3ef28c864cef1f5c96cb5457e427ac0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.736ex; height:2.509ex;" alt="{\displaystyle Leq}" loading="lazy"> can be defined by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Leq=IsZero\circ Sub}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Leq=IsZero\circ Sub}</annotation>

</semantics>

</math><img src="./079ee1e4aeb35646f220f5d88e4529a8d0445e33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:20.058ex; height:2.509ex;" alt="{\displaystyle Leq=IsZero\circ Sub}" loading="lazy">. Then <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Leq(x,y)=1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Leq(x,y)=1}</annotation>

</semantics>

</math><img src="./f62f921bf7aa29584ce9e83668f8f1ec8092c080.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.325ex; height:2.843ex;" alt="{\displaystyle Leq(x,y)=1}" loading="lazy"> if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x\leq y}</annotation>

</semantics>

</math><img src="./c07a0bc023490be1c08e6c33a9cdc93bec908224.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle x\leq y}" loading="lazy">, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Leq(x,y)=0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Leq(x,y)=0}</annotation>

</semantics>

</math><img src="./c43c740ef880565882bd017101894f4abdb97871.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.325ex; height:2.843ex;" alt="{\displaystyle Leq(x,y)=0}" loading="lazy">, otherwise. As a computation example,

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

<mtext> by property of </mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

<mtext> by property of </mtext>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lll}&Leq(8,3)\\=&IsZero(Sub(8,3))&{\text{ by Def. }}Leq\\=&IsZero(5)&{\text{ by property of }}Sub\\=&0&{\text{ by property of }}IsZero\\\end{array}}}</annotation>

</semantics>

</math><img src="./e035b2f3b0ca5e36543ac006eb1a6edb5e0d8281.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -5.838ex; width:47.866ex; height:12.843ex;" alt="{\displaystyle {\begin{array}{lll}&Leq(8,3)\\=&IsZero(Sub(8,3))&{\text{ by Def. }}Leq\\=&IsZero(5)&{\text{ by property of }}Sub\\=&0&{\text{ by property of }}IsZero\\\end{array}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Predicate_"Greater_or_equal"">Predicate "Greater or equal"</h3></div>

Once a definition of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Leq}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Leq}</annotation>

</semantics>

</math><img src="./a976a2a3ef28c864cef1f5c96cb5457e427ac0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.736ex; height:2.509ex;" alt="{\displaystyle Leq}" loading="lazy"> is obtained, the converse predicate can be defined as <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Geq=Leq\circ (P_{2}^{2},P_{1}^{2})}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Geq=Leq\circ (P_{2}^{2},P_{1}^{2})}</annotation>

</semantics>

</math><img src="./ffc387d34487a360460f9715ea43665de1f0e5a1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:21.604ex; height:3.176ex;" alt="{\displaystyle Geq=Leq\circ (P_{2}^{2},P_{1}^{2})}" loading="lazy">. Then, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Geq(x,y)=Leq(y,x)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Geq(x,y)=Leq(y,x)}</annotation>

</semantics>

</math><img src="./6fc5b3b3dbf83b94a633339cd4118d55b4a4d509.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.471ex; height:2.843ex;" alt="{\displaystyle Geq(x,y)=Leq(y,x)}" loading="lazy"> is true (more precisely: has value 1) if, and only if, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\geq y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x\geq y}</annotation>

</semantics>

</math><img src="./aded94d634c48071188bf96a76a4d3b7dfb28470.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle x\geq y}" loading="lazy">.

The 3-ary if-then-else operator known from programming languages can be defined by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\textit {If}}=\rho (P_{2}^{2},P_{3}^{4})}">

</mrow>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\textit {If}}=\rho (P_{2}^{2},P_{3}^{4})}</annotation>

</semantics>

</math><img src="./05a6f7483233586794b1c629ef6c7fb0e07c607a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:14.507ex; height:3.176ex;" alt="{\displaystyle {\textit {If}}=\rho (P_{2}^{2},P_{3}^{4})}" loading="lazy">. Then, for arbitrary <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">,

<mtr>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lll}&{\textit {If}}(S(x),y,z)\\=&\rho (P_{2}^{2},P_{3}^{4})\;(S(x),y,z)&{\text{ by Def. }}{\textit {If}}\\=&P_{3}^{4}(x,{\textit {If}}(x,y,z),y,z)&{\text{ by case }}\rho (S(...),...)\\=&y&{\text{ by Def. }}P_{3}^{4}\\\end{array}}}</annotation>

</semantics>

</math><img src="./9ba6bd3cd44065b8da4d5cb1d9567443f3635ab9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -6.338ex; width:50.368ex; height:13.843ex;" alt="{\displaystyle {\begin{array}{lll}&{\textit {If}}(S(x),y,z)\\=&\rho (P_{2}^{2},P_{3}^{4})\;(S(x),y,z)&{\text{ by Def. }}{\textit {If}}\\=&P_{3}^{4}(x,{\textit {If}}(x,y,z),y,z)&{\text{ by case }}\rho (S(...),...)\\=&y&{\text{ by Def. }}P_{3}^{4}\\\end{array}}}" loading="lazy"></dd></dl>

and

<mtr>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</msubsup>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mrow>

</mrow>

</mrow>

</msubsup>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{lll}&{\textit {If}}(0,y,z)\\=&\rho (P_{2}^{2},P_{3}^{4})\;(0,y,z)&{\text{ by Def. }}{\textit {If}}\\=&P_{2}^{2}(y,z)&{\text{ by case }}\rho (0,...)\\=&z&{\text{ by Def. }}P_{2}^{2}.\\\end{array}}}</annotation>

</semantics>

</math><img src="./24e2e6c188e3e2f9b33ceaf89711b00ab5f04581.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -6.171ex; width:41.645ex; height:13.509ex;" alt="{\displaystyle {\begin{array}{lll}&{\textit {If}}(0,y,z)\\=&\rho (P_{2}^{2},P_{3}^{4})\;(0,y,z)&{\text{ by Def. }}{\textit {If}}\\=&P_{2}^{2}(y,z)&{\text{ by case }}\rho (0,...)\\=&z&{\text{ by Def. }}P_{2}^{2}.\\\end{array}}}" loading="lazy">.</dd></dl>

That is, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\textit {If}}(x,y,z)}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\textit {If}}(x,y,z)}</annotation>

</semantics>

</math><img src="./eb61b1c6db24c5603815831a1f1f7d463488527a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.062ex; height:2.843ex;" alt="{\displaystyle {\textit {If}}(x,y,z)}" loading="lazy"> returns the then-part, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">, if the if-part, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy">, is true, and the else-part, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle z}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle z}</annotation>

</semantics>

</math><img src="./bf368e72c009decd9b6686ee84a375632e11de98.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.088ex; height:1.676ex;" alt="{\displaystyle z}" loading="lazy">, otherwise.

<div class="mw-heading mw-heading3"><h3 id="Junctors">Junctors</h3></div>

Based on the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\textit {If}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\textit {If}}}</annotation>

</semantics>

</math><img src="./6e9820162706c72829a2429b2874e866d85531d7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-right: -0.332ex; width:1.944ex; height:2.509ex;" alt="{\displaystyle {\textit {If}}}" loading="lazy"> function, it is easy to define logical junctors. For example, defining <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle And={\textit {If}}\circ (P_{1}^{2},P_{2}^{2},C_{0}^{2})}">

</mrow>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle And={\textit {If}}\circ (P_{1}^{2},P_{2}^{2},C_{0}^{2})}</annotation>

</semantics>

</math><img src="./553b8985d8a11b2affbfceded045cfcdc8454c18.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:23.739ex; height:3.176ex;" alt="{\displaystyle And={\textit {If}}\circ (P_{1}^{2},P_{2}^{2},C_{0}^{2})}" loading="lazy">, one obtains <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle And(x,y)={\textit {If}}(x,y,0)}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle And(x,y)={\textit {If}}(x,y,0)}</annotation>

</semantics>

</math><img src="./1a42738a9431995e52c30a779f121b45ff1bb5b1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.917ex; height:2.843ex;" alt="{\displaystyle And(x,y)={\textit {If}}(x,y,0)}" loading="lazy">, that is, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle And(x,y)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle And(x,y)}</annotation>

</semantics>

</math><img src="./3d0b038815ea825217f10e86611542c33748fc2a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.682ex; height:2.843ex;" alt="{\displaystyle And(x,y)}" loading="lazy"> is true <a href="If%2C_and_only_if" class="mw-redirect" title="If, and only if">if, and only if</a>, both <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy"> are true (<a href="Logical_conjunction" title="Logical conjunction">logical conjunction</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">).

Similarly, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Or={\textit {If}}\circ (P_{1}^{2},C_{1}^{2},P_{2}^{2})}">

</mrow>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Or={\textit {If}}\circ (P_{1}^{2},C_{1}^{2},P_{2}^{2})}</annotation>

</semantics>

</math><img src="./45a9a024f653da5d05fc3d0774352179465e36ea.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:22.208ex; height:3.176ex;" alt="{\displaystyle Or={\textit {If}}\circ (P_{1}^{2},C_{1}^{2},P_{2}^{2})}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Not={\textit {If}}\circ (P_{1}^{1},C_{0}^{1},C_{1}^{1})}">

</mrow>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Not={\textit {If}}\circ (P_{1}^{1},C_{0}^{1},C_{1}^{1})}</annotation>

</semantics>

</math><img src="./2908404bbe99681cfdaa652a31c41ade89fe6fb7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:23.393ex; height:3.176ex;" alt="{\displaystyle Not={\textit {If}}\circ (P_{1}^{1},C_{0}^{1},C_{1}^{1})}" loading="lazy"> lead to appropriate definitions of <a href="Disjunction" class="mw-redirect" title="Disjunction">disjunction</a> and <a href="Negation" title="Negation">negation</a>: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Or(x,y)={\textit {If}}(x,1,y)}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Or(x,y)={\textit {If}}(x,1,y)}</annotation>

</semantics>

</math><img src="./4296ae6356a7f42b289c783487a688a27b4b0fe1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.385ex; height:2.843ex;" alt="{\displaystyle Or(x,y)={\textit {If}}(x,1,y)}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Not(x)={\textit {If}}(x,0,1)}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Not(x)={\textit {If}}(x,0,1)}</annotation>

</semantics>

</math><img src="./31ef8a046e8869540b2861226a93569532a43f7e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.412ex; height:2.843ex;" alt="{\displaystyle Not(x)={\textit {If}}(x,0,1)}" loading="lazy">.

<div class="mw-heading mw-heading3"><h3 id="Equality_predicate">Equality predicate</h3></div>

Using the above functions <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Leq}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Leq}</annotation>

</semantics>

</math><img src="./a976a2a3ef28c864cef1f5c96cb5457e427ac0dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.736ex; height:2.509ex;" alt="{\displaystyle Leq}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Geq}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Geq}</annotation>

</semantics>

</math><img src="./5ede08b8c8c34e5706cc45b5e08790ceca310aca.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.98ex; height:2.509ex;" alt="{\displaystyle Geq}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle And}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle And}</annotation>

</semantics>

</math><img src="./c2984c0459da7aaecd7054ec869c4527a1b20eac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.354ex; height:2.176ex;" alt="{\displaystyle And}" loading="lazy">, the definition <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Eq=And\circ (Leq,Geq)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Eq=And\circ (Leq,Geq)}</annotation>

</semantics>

</math><img src="./d00cb9a4c6ea70534bf5c9497e3606d922759022.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:23.051ex; height:2.843ex;" alt="{\displaystyle Eq=And\circ (Leq,Geq)}" loading="lazy"> implements the equality predicate. In fact, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Eq(x,y)=And(Leq(x,y),Geq(x,y))}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Eq(x,y)=And(Leq(x,y),Geq(x,y))}</annotation>

</semantics>

</math><img src="./5950d4e567872c691bc16bb257d0a89bcfd33cb6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:36.841ex; height:2.843ex;" alt="{\displaystyle Eq(x,y)=And(Leq(x,y),Geq(x,y))}" loading="lazy"> is true if, and only if, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> equals <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle y}</annotation>

</semantics>

</math><img src="./b8a6208ec717213d4317e666f1ae872e00620a0d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}" loading="lazy">.

Similarly, the definition <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Lt=Not\circ Geq}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Lt=Not\circ Geq}</annotation>

</semantics>

</math><img src="./fc5d7240bd2f8c9d7884faa648bbf902f682fef4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:15.726ex; height:2.509ex;" alt="{\displaystyle Lt=Not\circ Geq}" loading="lazy"> implements the predicate "less-than", and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle Gt=Not\circ Leq}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Gt=Not\circ Leq}</annotation>

</semantics>

</math><img src="./32ba85e321f2a83451a98969900ecb11265e64ef.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:15.726ex; height:2.509ex;" alt="{\displaystyle Gt=Not\circ Leq}" loading="lazy"> implements "greater-than".

<div class="mw-heading mw-heading3"><h3 id="Other_operations_on_natural_numbers">Other operations on natural numbers</h3></div>

<a href="Exponentiation" title="Exponentiation">Exponentiation</a> and <a href="Primality_test" title="Primality test">primality testing</a> are primitive recursive. Given primitive recursive functions <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle e}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle e}</annotation>

</semantics>

</math><img src="./cd253103f0876afc68ebead27a5aa9867d927467.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.083ex; height:1.676ex;" alt="{\displaystyle e}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f}</annotation>

</semantics>

</math><img src="./132e57acb643253e7810ee9702d9581f159a1c61.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g}</annotation>

</semantics>

</math><img src="./d3556280e66fe2c0d0140df20935a6f057381d77.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.116ex; height:2.009ex;" alt="{\displaystyle g}" loading="lazy">, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy">, a function that returns the value of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g}</annotation>

</semantics>

</math><img src="./d3556280e66fe2c0d0140df20935a6f057381d77.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.116ex; height:2.009ex;" alt="{\displaystyle g}" loading="lazy"> when <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle e\leq f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle e\leq f}</annotation>

</semantics>

</math><img src="./795281fe9b79eda9ca0b4c5132951d284c2d2f64.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.461ex; height:2.509ex;" alt="{\displaystyle e\leq f}" loading="lazy"> and the value of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"> otherwise is primitive recursive.

<div class="mw-heading mw-heading3"><h3 id="Operations_on_integers_and_rational_numbers">Operations on integers and rational numbers</h3></div>

By using <a href="G%C3%B6del_numbering" title="Gödel numbering">Gödel numberings</a>, the primitive recursive functions can be extended to operate on other objects such as integers and <a href="Rational_number" title="Rational number">rational numbers</a>. If integers are encoded by Gödel numbers in a standard way, the arithmetic operations including addition, subtraction, and multiplication are all primitive recursive. Similarly, if the rationals are represented by Gödel numbers then the <a href="Field_(mathematics)" title="Field (mathematics)">field</a> operations are all primitive recursive.

<div class="mw-heading mw-heading3"><h3 id="Some_common_primitive_recursive_functions">Some common primitive recursive functions</h3></div>

The following examples and definitions are from <a href="#CITEREFKleene1974">Kleene 1974</a>, pp. 222–231. Many appear with proofs. Most also appear with similar names, either as proofs or as examples, in <a href="#CITEREFBoolosBurgessJeffrey2002">Boolos, Burgess & Jeffrey 2002</a>, pp. 63–70 they add the logarithm lo(x, y) or lg(x, y) depending on the exact derivation.

In the following the mark " ' ", e.g. a', is the primitive mark meaning "the successor of", usually thought of as " +1", e.g. a +1 =def a'. The functions 16–20 and #G are of particular interest with respect to converting primitive recursive predicates to, and extracting them from, their "arithmetical" form expressed as <a href="G%C3%B6del_number" class="mw-redirect" title="Gödel number">Gödel numbers</a>.

<dl><dd><ol><li>Addition: a+b</li>

<li>Multiplication: a×b</li>

<li>Exponentiation: ab</li>

<li>Factorial a! : 0! = 1, a'! = a!×a'</li>

<li>pred(a): (Predecessor or decrement): If a > 0 then a−1 else 0</li>

<li>Proper subtraction a ∸ b: If a ≥ b then a−b else 0</li>

<li>Minimum(a1, ... an)</li>

<li>Maximum(a1, ... an)</li>

<li>Absolute difference: | a−b | =def (a ∸ b) + (b ∸ a)</li>

<li>~sg(a): NOT[signum(a)]: If a=0 then 1 else 0</li>

<li>sg(a): signum(a): If a=0 then 0 else 1</li>

<li>a | b: (a divides b): If b=k×a for some k then 0 else 1</li>

<li>Remainder(a, b): the leftover if b does not divide a "evenly". Also called MOD(a, b)</li>

<li>a = b: sg | a − b | (Kleene's convention was to represent true by 0 and false by 1; presently, especially in computers, the most common convention is the reverse, namely to represent true by 1 and false by 0, which amounts to changing sg into ~sg here and in the next item)</li>

<li>Pr(a): a is a prime number Pr(a) =def a>1 & NOT(Exists c)1<c<a [ c|a ]</li>

<li>pi: the i+1th prime number</li>

<li>(a)i: exponent of pi in a: the unique x such that pix|a & NOT(pix'|a)</li>

<li>lh(a): the "length" or number of non-vanishing exponents in a</li>

<li>lo(a, b): (logarithm of a to base b): If a, b > 1 then the greatest x such that bx | a else 0</li></ol></dd></dl>

<dl><dd>In the following, the abbreviation x =def x1, ... xn; subscripts may be applied if the meaning requires.</dd></dl>

<ul><li>#A: A function φ definable explicitly from functions Ψ and constants q1, ... qn is primitive recursive in Ψ.</li>

<li>#B: The finite sum Σy<z ψ(x, y) and product Πy<zψ(x, y) are primitive recursive in ψ.</li>

<li>#C: A predicate P obtained by substituting functions χ1,..., χm for the respective variables of a predicate Q is primitive recursive in χ1,..., χm, Q.</li>

<li>#D: The following predicates are primitive recursive in Q and R:</li></ul>

<li>Q IMPLIES R: Q(x) → R(x)</li>

<li>Q is equivalent to R: Q(x) ≡ R(x)</li></ul></dd></dl></dd></dl>

<ul><li>#E: The following predicates are primitive recursive in the predicate R:</li></ul>

<li>μyy<z R(x, y). The operator μyy<z R(x, y) is a bounded form of the so-called minimization- or <a href="Mu-operator" class="mw-redirect" title="Mu-operator">mu-operator</a>: Defined as "the least value of y less than z such that R(x, y) is true; or z if there is no such value."</li></ul></dd></dl></dd></dl>

<ul><li>#F: Definition by cases: The function defined thus, where Q1, ..., Qm are mutually exclusive predicates (or "ψ(x) shall have the value given by the first clause that applies), is primitive recursive in φ1, ..., Q1, ... Qm:</li></ul>

<dl><dd><dl><dd>φ(x) =

<li>φm+1(x) otherwise</li></ul></dd></dl></dd></dl>

<ul><li>#G: If φ satisfies the equation:</li></ul>

<dl><dd><dl><dd>φ(y,x) = χ(y, COURSE-φ(y; x2, ... xn ), x2, ... xn then φ is primitive recursive in χ. The value COURSE-φ(y; x2 to n ) of the course-of-values function encodes the sequence of values φ(0,x2 to n), ..., φ(y-1,x2 to n) of the original function.</dd></dl></dd></dl>

<div class="mw-heading mw-heading2"><h2 id="Relationship_to_recursive_functions">Relationship to recursive functions</h2></div>

The broader class of <a href="Partial_recursive_function" class="mw-redirect" title="Partial recursive function">partial recursive functions</a> is defined by introducing an <a href="Mu_operator" class="mw-redirect" title="Mu operator">unbounded search operator</a>. The use of this operator may result in a <a href="Partial_function" title="Partial function">partial function</a>, that is, a relation with at most one value for each argument, but does not necessarily have any value for any argument (see <a href="Domain_of_a_function" title="Domain of a function">domain</a>). An equivalent definition states that a partial recursive function is one that can be computed by a <a href="Turing_machine" title="Turing machine">Turing machine</a>. A total recursive function is a partial recursive function that is defined for every input.

Every primitive recursive function is total recursive, but not all total recursive functions are primitive recursive. The <a href="Ackermann_function" title="Ackermann function">Ackermann function</a> A(m,n) is a well-known example of a total recursive function (in fact, provable total), that is not primitive recursive. There is a characterization of the primitive recursive functions as a subset of the total recursive functions using the Ackermann function. This characterization states that a function is primitive recursive <a href="If_and_only_if" title="If and only if">if and only if</a> there is a natural number m such that the function can be computed by a Turing <a href="Machine_that_always_halts" class="mw-redirect" title="Machine that always halts">machine that always halts</a> within A(m,n) or fewer steps, where n is the sum of the arguments of the primitive recursive function.<a href="#cite_note-6">[6]</a>

An important property of the primitive recursive functions is that they are a <a href="Recursively_enumerable" class="mw-redirect" title="Recursively enumerable">recursively enumerable</a> subset of the set of all <a href="Total_recursive_function" class="mw-redirect" title="Total recursive function">total recursive functions</a> (which is not itself recursively enumerable). This means that there is a single computable function f(m,n) that enumerates the primitive recursive functions, namely:

<ul><li>For every primitive recursive function g, there is an m such that g(n) = f(m,n) for all n, and</li>

<li>For every m, the function h(n) = f(m,n) is primitive recursive.</li></ul>

f can be explicitly constructed by iteratively repeating all possible ways of creating primitive recursive functions. Thus, it is provably total. One can use a <a href="Diagonal_lemma" title="Diagonal lemma">diagonalization</a> argument to show that f is not recursive primitive in itself: had it been such, so would be h(n) = f(n,n)+1. But if this equals some primitive recursive function, there is an m such that h(n) = f(m,n) for all n, and then h(m) = f(m,m), leading to contradiction.

However, the set of primitive recursive functions is not the largest recursively enumerable subset of the set of all total recursive functions. For example, the set of provably total functions (in Peano arithmetic) is also recursively enumerable, as one can enumerate all the proofs of the theory. While all primitive recursive functions are provably total, the converse is not true.

<div class="mw-heading mw-heading2"><h2 id="Limitations">Limitations</h2></div>

Primitive recursive functions tend to correspond very closely with our intuition of what a computable function must be. Certainly the initial functions are intuitively computable (in their very simplicity), and the two operations by which one can create new primitive recursive functions are also very straightforward. However, the set of primitive recursive functions does not include every possible total computable function—this can be seen with a variant of <a href="Cantor's_diagonal_argument" title="Cantor's diagonal argument">Cantor's diagonal argument</a>. This argument provides a total computable function that is not primitive recursive. A sketch of the proof is as follows:

/* start https://en.wikipedia.org/ */

.mw-parser-output .block-indent{padding-left:3em;padding-right:0;overflow:hidden}

/* end https://en.wikipedia.org/ */

</style><div class="block-indent">The primitive recursive functions of one argument (i.e., unary functions) can be <a href="Recursively_enumerable_set" class="mw-redirect" title="Recursively enumerable set">computably enumerated</a>. This enumeration uses the definitions of the primitive recursive functions (which are essentially just expressions with the composition and primitive recursion operations as operators and the basic primitive recursive functions as atoms), and can be assumed to contain every definition once, even though a same function will occur many times on the list (since many definitions define the same function; indeed simply composing by the <a href="Identity_function" title="Identity function">identity function</a> generates infinitely many definitions of any one primitive recursive function). This means that the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy">-th definition of a primitive recursive function in this enumeration can be effectively determined from <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy">. Indeed if one uses some <a href="G%C3%B6del_numbering" title="Gödel numbering">Gödel numbering</a> to encode definitions as numbers, then this <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy">-th definition in the list is computed by a primitive recursive function of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy">. Let <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f_{n}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f_{n}}</annotation>

</semantics>

</math><img src="./b2702450f0458a5e01a698e248af552a7fab2b50.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.358ex; height:2.509ex;" alt="{\displaystyle f_{n}}" loading="lazy"> denote the unary primitive recursive function given by this definition.

Now define the "evaluator function" <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ev}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ev}</annotation>

</semantics>

</math><img src="./c9e901132d15fa7733d1458e7926ba558a7945c0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.211ex; height:1.676ex;" alt="{\displaystyle ev}" loading="lazy"> with two arguments, by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ev(i,j)=f_{i}(j)}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ev(i,j)=f_{i}(j)}</annotation>

</semantics>

</math><img src="./b7176019cf50e992f29216a260c45c3b93640aa3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.62ex; height:2.843ex;" alt="{\displaystyle ev(i,j)=f_{i}(j)}" loading="lazy">. Clearly <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ev}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ev}</annotation>

</semantics>

</math><img src="./c9e901132d15fa7733d1458e7926ba558a7945c0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.211ex; height:1.676ex;" alt="{\displaystyle ev}" loading="lazy"> is total and computable, since one can effectively determine the definition of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f_{i}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f_{i}}</annotation>

</semantics>

</math><img src="./65da883ca3d16b461e46c94777b0d9c4aa010e79.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.939ex; height:2.509ex;" alt="{\displaystyle f_{i}}" loading="lazy">, and being a primitive recursive function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f_{i}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f_{i}}</annotation>

</semantics>

</math><img src="./65da883ca3d16b461e46c94777b0d9c4aa010e79.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.939ex; height:2.509ex;" alt="{\displaystyle f_{i}}" loading="lazy"> is itself total and computable, so <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f_{i}(j)}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f_{i}(j)}</annotation>

</semantics>

</math><img src="./ebecb21e8503ac411e9a0de08c5eb8112a5839a8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.706ex; height:2.843ex;" alt="{\displaystyle f_{i}(j)}" loading="lazy"> is always defined and effectively computable. However a diagonal argument will show that the function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ev}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ev}</annotation>

</semantics>

</math><img src="./c9e901132d15fa7733d1458e7926ba558a7945c0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.211ex; height:1.676ex;" alt="{\displaystyle ev}" loading="lazy"> of two arguments is not primitive recursive.

Suppose <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ev}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ev}</annotation>

</semantics>

</math><img src="./c9e901132d15fa7733d1458e7926ba558a7945c0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.211ex; height:1.676ex;" alt="{\displaystyle ev}" loading="lazy"> were primitive recursive, then the unary function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g}</annotation>

</semantics>

</math><img src="./d3556280e66fe2c0d0140df20935a6f057381d77.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.116ex; height:2.009ex;" alt="{\displaystyle g}" loading="lazy"> defined by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g(i)=S(ev(i,i))}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g(i)=S(ev(i,i))}</annotation>

</semantics>

</math><img src="./a9b82dff3bb46d7fe31849576cfb4a693fdb2fe9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.794ex; height:2.843ex;" alt="{\displaystyle g(i)=S(ev(i,i))}" loading="lazy"> would also be primitive recursive, as it is defined by composition from the successor function and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ev}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle ev}</annotation>

</semantics>

</math><img src="./c9e901132d15fa7733d1458e7926ba558a7945c0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.211ex; height:1.676ex;" alt="{\displaystyle ev}" loading="lazy">. But then <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g}</annotation>

</semantics>

</math><img src="./d3556280e66fe2c0d0140df20935a6f057381d77.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.116ex; height:2.009ex;" alt="{\displaystyle g}" loading="lazy"> occurs in the enumeration, so there is some number <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy"> such that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g=f_{n}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g=f_{n}}</annotation>

</semantics>

</math><img src="./103493a6d369c80aa5688a2a4308fb6a2b023bcd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.572ex; height:2.509ex;" alt="{\displaystyle g=f_{n}}" loading="lazy">. But now <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle g(n)=S(ev(n,n))=S(f_{n}(n))=S(g(n))}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g(n)=S(ev(n,n))=S(f_{n}(n))=S(g(n))}</annotation>

</semantics>

</math><img src="./81b5d1bac6f776de46fdb12a5219af752084b7f7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:41.266ex; height:2.843ex;" alt="{\displaystyle g(n)=S(ev(n,n))=S(f_{n}(n))=S(g(n))}" loading="lazy"> gives a contradiction.</div>

This argument can be applied to any class of computable (total) functions that can be enumerated in this way, as explained in the article <a href="Machine_that_always_halts" class="mw-redirect" title="Machine that always halts">Machine that always halts</a>. Note however that the partial computable functions (those that need not be defined for all arguments) can be explicitly enumerated, for instance by enumerating Turing machine encodings.

Other examples of total recursive but not primitive recursive functions are known:

<ul><li>The function that takes m to <a href="Ackermann_function" title="Ackermann function">Ackermann</a>(m,m) is a unary total recursive function that is not primitive recursive.</li>

<li>The <a href="Paris%E2%80%93Harrington_theorem" title="Paris–Harrington theorem">Paris–Harrington theorem</a> involves a total recursive function that is not primitive recursive.</li>

<li>The <a href="Sudan_function" title="Sudan function">Sudan function</a></li>

<li>The <a href="Goodstein_function" class="mw-redirect" title="Goodstein function">Goodstein function</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Variants">Variants</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Constant_functions">Constant functions</h3></div>

Instead of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{n}^{k}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{n}^{k}}</annotation>

</semantics>

</math><img src="./9b088b67f00e4739e57c658ac7dd5913898013ac.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.887ex; height:2.843ex;" alt="{\displaystyle C_{n}^{k}}" loading="lazy">,

alternative definitions use just one 0-ary zero function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle C_{0}^{0}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle C_{0}^{0}}</annotation>

</semantics>

</math><img src="./1de12f06a3041941e852c046cf9b4ce17974bf19.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.852ex; height:3.176ex;" alt="{\displaystyle C_{0}^{0}}" loading="lazy"> as a primitive function that always returns zero, and built the constant functions from the zero function, the successor function and the composition operator.

<div class="mw-heading mw-heading3"><h3 id="Iterative_functions">Iterative functions</h3></div>

Robinson<a href="#cite_note-FOOTNOTERobinson1947-7">[7]</a> considered various restrictions of the recursion rule. One is the so-called iteration rule where the function h does not have access to the parameters xi (in this case, we may assume without loss of generality that the function g is just the identity, as the general case can be obtained by substitution):

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}f(0,x)&=x,\\f(S(y),x)&=h(y,f(y,x)).\end{aligned}}}</annotation>

</semantics>

</math><img src="./50e6ebf9b39f3878a723882947b44b341da22d88.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:26.357ex; height:6.176ex;" alt="{\displaystyle {\begin{aligned}f(0,x)&=x,\\f(S(y),x)&=h(y,f(y,x)).\end{aligned}}}" loading="lazy"></dd></dl>

He proved that the class of all primitive recursive functions can still be obtained in this way.

<div class="mw-heading mw-heading3"><h3 id="Pure_recursion">Pure recursion</h3></div>

Another restriction considered by Robinson<a href="#cite_note-FOOTNOTERobinson1947-7">[7]</a> is pure recursion, where h does not have access to the induction variable y:

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}f(0,x_{1},\ldots ,x_{k})&=g(x_{1},\ldots ,x_{k}),\\f(S(y),x_{1},\ldots ,x_{k})&=h(f(y,x_{1},\ldots ,x_{k}),x_{1},\ldots ,x_{k}).\end{aligned}}}</annotation>

</semantics>

</math><img src="./03a846452f10e63ce61c74b1ad451be81eb72890.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:52.484ex; height:6.176ex;" alt="{\displaystyle {\begin{aligned}f(0,x_{1},\ldots ,x_{k})&=g(x_{1},\ldots ,x_{k}),\\f(S(y),x_{1},\ldots ,x_{k})&=h(f(y,x_{1},\ldots ,x_{k}),x_{1},\ldots ,x_{k}).\end{aligned}}}" loading="lazy"></dd></dl>

Gladstone<a href="#cite_note-FOOTNOTEGladstone1967-8">[8]</a> proved that this rule is enough to generate all primitive recursive functions. Gladstone<a href="#cite_note-FOOTNOTEGladstone1971-9">[9]</a> improved this so that even the combination of these two restrictions, i.e., the pure iteration rule below, is enough:

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}f(0,x)&=x,\\f(S(y),x)&=h(f(y,x)).\end{aligned}}}</annotation>

</semantics>

</math><img src="./210b3de7483bb1ba5e9790931ddd9938b64ef954.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:24.168ex; height:6.176ex;" alt="{\displaystyle {\begin{aligned}f(0,x)&=x,\\f(S(y),x)&=h(f(y,x)).\end{aligned}}}" loading="lazy"></dd></dl>

Further improvements are possible: Severin<a href="#cite_note-FOOTNOTESeverin2008-10">[10]</a> prove that even the pure iteration rule without parameters, namely

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}f(0)&=0,\\f(S(y))&=h(f(y)),\end{aligned}}}</annotation>

</semantics>

</math><img src="./b34513a694e7266021a1c3099cba2c2d622054f2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:19.44ex; height:6.176ex;" alt="{\displaystyle {\begin{aligned}f(0)&=0,\\f(S(y))&=h(f(y)),\end{aligned}}}" loading="lazy"></dd></dl>

suffices to generate all <a href="Unary_operation" title="Unary operation">unary</a> primitive recursive functions if we extend the set of initial functions with truncated subtraction x ∸ y. We get all primitive recursive functions if we additionally include + as an initial function.

<div class="mw-heading mw-heading3"><h3 id="Additional_primitive_recursive_forms">Additional primitive recursive forms</h3></div>

Some additional forms of recursion also define functions that are in fact

primitive recursive. Definitions in these forms may be easier to find or

more natural for reading or writing. <a href="Course-of-values_recursion" title="Course-of-values recursion">Course-of-values recursion</a> defines primitive recursive functions. Some forms of <a href="Mutual_recursion" title="Mutual recursion">mutual recursion</a> also define primitive recursive functions.

The functions that can be programmed in the <a href="LOOP_(programming_language)" title="LOOP (programming language)">LOOP programming language</a> are exactly the primitive recursive functions. This gives a different characterization of the power of these functions. The main limitation of the LOOP language, compared to a <a href="Turing-complete_language" class="mw-redirect" title="Turing-complete language">Turing-complete language</a>, is that in the LOOP language the number of times that each loop will run is specified before the loop begins to run.

<div class="mw-heading mw-heading3"><h3 id="Computer_language_definition">Computer language definition</h3></div>

An example of a primitive recursive programming language is one that contains basic arithmetic operators (e.g. + and −, or ADD and SUBTRACT), conditionals and comparison (IF-THEN, EQUALS, LESS-THAN), and bounded loops, such as the basic <a href="For_loop" title="For loop">for loop</a>, where there is a known or calculable upper bound to all loops (FOR i FROM 1 TO n, with neither i nor n modifiable by the loop body). No control structures of greater generality, such as <a href="While_loop" title="While loop">while loops</a> or IF-THEN plus <a href="GOTO" class="mw-redirect" title="GOTO">GOTO</a>, are admitted in a primitive recursive language.

The <a href="LOOP_(programming_language)" title="LOOP (programming language)">LOOP language</a>, introduced in a 1967 paper by <a href="Albert_R._Meyer" title="Albert R. Meyer">Albert R. Meyer</a> and <a href="Dennis_M._Ritchie" class="mw-redirect" title="Dennis M. Ritchie">Dennis M. Ritchie</a>,<a href="#cite_note-11">[11]</a> is such a language. Its computing power coincides with the primitive recursive functions. A variant of the LOOP language is <a href="Douglas_Hofstadter" title="Douglas Hofstadter">Douglas Hofstadter</a>'s <a href="BlooP_and_FlooP" title="BlooP and FlooP">BlooP</a> in <a href="G%C3%B6del%2C_Escher%2C_Bach" title="Gödel, Escher, Bach">Gödel, Escher, Bach</a>. Adding unbounded loops (WHILE, GOTO) makes the language <a href="General_recursive_function" title="General recursive function">general recursive</a> and <a href="Turing_completeness" title="Turing completeness">Turing-complete</a>, as are all real-world computer programming languages.

The definition of primitive recursive functions implies that their computation halts on every input (after a finite number of steps). On the other hand, the <a href="Halting_problem" title="Halting problem">halting problem</a> is <a href="Undecidable_problem" title="Undecidable problem">undecidable</a> for general recursive functions.

<div class="mw-heading mw-heading2"><h2 id="Finitism_and_consistency_results">Finitism and consistency results</h2></div>

The primitive recursive functions are closely related to mathematical <a href="Finitism" title="Finitism">finitism</a>, and are used in several contexts in mathematical logic where a particularly constructive system is desired. <a href="Primitive_recursive_arithmetic" title="Primitive recursive arithmetic">Primitive recursive arithmetic</a> (PRA), a formal axiom system for the natural numbers and the primitive recursive functions on them, is often used for this purpose.

PRA is much weaker than <a href="Peano_arithmetic" class="mw-redirect" title="Peano arithmetic">Peano arithmetic</a>, which is not a finitistic system. Nevertheless, many results in <a href="Number_theory" title="Number theory">number theory</a> and in <a href="Proof_theory" title="Proof theory">proof theory</a> can be proved in PRA. For example, <a href="G%C3%B6del's_incompleteness_theorem" class="mw-redirect" title="Gödel's incompleteness theorem">Gödel's incompleteness theorem</a> can be formalized into PRA, giving the following theorem:

<dl><dd>If T is a theory of arithmetic satisfying certain hypotheses, with Gödel sentence GT, then PRA proves the implication Con(T)→GT.</dd></dl>

Similarly, many of the syntactic results in proof theory can be proved in PRA, which implies that there are primitive recursive functions that carry out the corresponding syntactic transformations of proofs.

In proof theory and <a href="Set_theory" title="Set theory">set theory</a>, there is an interest in finitistic <a href="Consistency_proof" class="mw-redirect" title="Consistency proof">consistency proofs</a>, that is, consistency proofs that themselves are finitistically acceptable. Such a proof establishes that the consistency of a theory T implies the consistency of a theory S by producing a primitive recursive function that can transform any proof of an inconsistency from S into a proof of an inconsistency from T. One sufficient condition for a consistency proof to be finitistic is the ability to formalize it in PRA. For example, many consistency results in set theory that are obtained by <a href="Forcing_(mathematics)" title="Forcing (mathematics)">forcing</a> can be recast as syntactic proofs that can be formalized in PRA.

<div class="mw-heading mw-heading2"><h2 id="History">History</h2></div>

<a href="Recursive_definition" title="Recursive definition">Recursive definitions</a> had been used more or less formally in mathematics before, but the construction of primitive recursion is traced back to <a href="Richard_Dedekind" title="Richard Dedekind">Richard Dedekind</a>'s theorem 126 of his Was sind und was sollen die Zahlen? (1888). This work was the first to give a proof that a certain recursive construction defines a unique function.<a href="#cite_note-Smith2013-12">[12]</a><a href="#cite_note-Tourlakis2003-13">[13]</a><a href="#cite_note-Downey2014-14">[14]</a>

<a href="Primitive_recursive_arithmetic" title="Primitive recursive arithmetic">Primitive recursive arithmetic</a> was first proposed by <a href="Thoralf_Skolem" title="Thoralf Skolem">Thoralf Skolem</a><a href="#cite_note-15">[15]</a> in 1923.

The current terminology was coined by <a href="R%C3%B3zsa_P%C3%A9ter" title="Rózsa Péter">Rózsa Péter</a> (1934) after <a href="Wilhelm_Ackermann" title="Wilhelm Ackermann">Ackermann</a> had proved in 1928 that the function which today is named after him was not primitive recursive, an event which prompted the need to rename what until then were simply called recursive functions.<a href="#cite_note-Tourlakis2003-13">[13]</a><a href="#cite_note-Downey2014-14">[14]</a>

<ul><li><a href="Grzegorczyk_hierarchy" title="Grzegorczyk hierarchy">Grzegorczyk hierarchy</a></li>

<li><a href="Recursion_(computer_science)" title="Recursion (computer science)">Recursion (computer science)</a></li>

<li><a href="Primitive_recursive_functional" title="Primitive recursive functional">Primitive recursive functional</a></li>

<li><a href="Double_recursion" title="Double recursion">Double recursion</a></li>

<li><a href="Primitive_recursive_set_function" title="Primitive recursive set function">Primitive recursive set function</a></li>

<li><a href="Primitive_recursive_ordinal_function" class="mw-redirect" title="Primitive recursive ordinal function">Primitive recursive ordinal function</a></li>

<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

<li id="cite_note-FOOTNOTEBrainerdLandweber1974-1"><a href="#cite_ref-FOOTNOTEBrainerdLandweber1974_1-0">^</a> <a href="#CITEREFBrainerdLandweber1974">Brainerd & Landweber 1974</a>.

</li>

<li id="cite_note-FOOTNOTEHartmanis1989-2"><a href="#cite_ref-FOOTNOTEHartmanis1989_2-0">^</a> <a href="#CITEREFHartmanis1989">Hartmanis 1989</a>.

</li>

<li id="cite_note-3"><a href="#cite_ref-3">^</a> <a href="#CITEREFPlanetMath">PlanetMath</a>

</li>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFHenk_Barendregt1990" class="citation cs2"><a href="Henk_Barendregt" title="Henk Barendregt">Henk Barendregt</a> (1990), "Functional Programming and Lambda Calculus", in <a href="Jan_van_Leeuwen" title="Jan van Leeuwen">Jan van Leeuwen</a> (ed.), Formal Models and Semantics, Handbook of Theoretical Computer Science, vol. B, Elsevier, pp. 321–364, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-444-88074-7</bdi></cite> Here: 2.2.6 initial functions, Def.2.2.7 primitive recursion, p.331-332.

</li>

<li id="cite_note-FOOTNOTEKleene1974226–227-5"><a href="#cite_ref-FOOTNOTEKleene1974226–227_5-0">^</a> <a href="#CITEREFKleene1974">Kleene 1974</a>, pp. 226–227.

</li>

<li id="cite_note-6"><a href="#cite_ref-6">^</a> This follows from the facts that the functions of this form are the most quickly growing primitive recursive functions, and that a function is primitive recursive if and only if its time complexity is bounded by a primitive recursive function. For the former, see <cite id="CITEREFLinz2011" class="citation cs2">Linz, Peter (2011), <a rel="nofollow" class="external text" href="https://books.google.com/books?id=hsxDiWvVdBcC&pg=PA332">An Introduction to Formal Languages and Automata</a>, Jones & Bartlett Publishers, p. 332, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9781449615529</bdi></cite>. For the latter, see <cite id="CITEREFMooreMertens2011" class="citation cs2"><a href="Cristopher_Moore" title="Cristopher Moore">Moore, Cristopher</a>; Mertens, Stephan (2011), <a rel="nofollow" class="external text" href="https://books.google.com/books?id=jnGKbpMV8xoC&pg=PA287">The Nature of Computation</a>, Oxford University Press, p. 287, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9780191620805</bdi></cite>

</li>

<li id="cite_note-FOOTNOTERobinson1947-7">^ <a href="#cite_ref-FOOTNOTERobinson1947_7-0">a</a> <a href="#cite_ref-FOOTNOTERobinson1947_7-1">b</a> <a href="#CITEREFRobinson1947">Robinson 1947</a>.

</li>

<li id="cite_note-FOOTNOTEGladstone1967-8"><a href="#cite_ref-FOOTNOTEGladstone1967_8-0">^</a> <a href="#CITEREFGladstone1967">Gladstone 1967</a>.

</li>

<li id="cite_note-FOOTNOTEGladstone1971-9"><a href="#cite_ref-FOOTNOTEGladstone1971_9-0">^</a> <a href="#CITEREFGladstone1971">Gladstone 1971</a>.

</li>

<li id="cite_note-FOOTNOTESeverin2008-10"><a href="#cite_ref-FOOTNOTESeverin2008_10-0">^</a> <a href="#CITEREFSeverin2008">Severin 2008</a>.

</li>

<li id="cite_note-11"><a href="#cite_ref-11">^</a> <cite id="CITEREFMeyerRitchie1967" class="citation cs2"><a href="Albert_R._Meyer" title="Albert R. Meyer">Meyer, Albert R.</a>; <a href="Dennis_Ritchie" title="Dennis Ritchie">Ritchie, Dennis M.</a> (1967), "The complexity of loop programs", ACM '67: Proceedings of the 1967 22nd national conference, pp. 465–469, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F800196.806014">10.1145/800196.806014</a></cite>

</li>

<li id="cite_note-Smith2013-12"><a href="#cite_ref-Smith2013_12-0">^</a> <cite id="CITEREFPeter_Smith2013" class="citation cs2">Peter Smith (2013), <a rel="nofollow" class="external text" href="https://www.logicmatters.net/igt/">An Introduction to Gödel's Theorems</a> (2nd ed.), Cambridge University Press, pp. 98–99, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-107-02284-3</bdi></cite>

</li>

<li id="cite_note-Tourlakis2003-13">^ <a href="#cite_ref-Tourlakis2003_13-0">a</a> <a href="#cite_ref-Tourlakis2003_13-1">b</a> <cite id="CITEREFGeorge_Tourlakis2003" class="citation cs2">George Tourlakis (2003), Lectures in Logic and Set Theory: Volume 1, Mathematical Logic, Cambridge University Press, p. 129, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-139-43942-8</bdi></cite>

</li>

<li id="cite_note-Downey2014-14">^ <a href="#cite_ref-Downey2014_14-0">a</a> <a href="#cite_ref-Downey2014_14-1">b</a> <cite id="CITEREFRod_Downey2014" class="citation cs2">Rod Downey, ed. (2014), Turing's Legacy: Developments from Turing's Ideas in Logic, Cambridge University Press, p. 474, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-107-04348-0</bdi></cite>

</li>

<li id="cite_note-15"><a href="#cite_ref-15">^</a> <a href="Thoralf_Skolem" title="Thoralf Skolem">Thoralf Skolem</a> (1923) "The foundations of elementary arithmetic" in <a href="Jean_van_Heijenoort" title="Jean van Heijenoort">Jean van Heijenoort</a>, translator and ed. (1967) From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press: 302-33.

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<ul><li><cite id="CITEREFBoolosBurgessJeffrey2002" class="citation book cs2"><a href="George_Boolos" title="George Boolos">Boolos, George</a>; <a href="John_P._Burgess" title="John P. Burgess">Burgess, John</a>; <a href="Richard_Jeffrey" title="Richard Jeffrey">Jeffrey, Richard C.</a> (2002), Computability and Logic (4th ed.), Cambridge University Press, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9780521007580</bdi></cite></li></ul>

<ul><li><cite id="CITEREFBrainerdLandweber1974" class="citation book cs2">Brainerd, W.S.; Landweber, L.H. (1974), Theory of Computation, Wiley, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0471095850</bdi></cite></li></ul>

<ul><li><cite id="CITEREFGladstone1967" class="citation journal cs2">Gladstone, M. D. (1967), "A reduction of the recursion scheme", The Journal of Symbolic Logic, 32 (4): 505–508, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.2307%2F2270177">10.2307/2270177</a>, <a href="JSTOR_(identifier)" class="mw-redirect" title="JSTOR (identifier)">JSTOR</a> <a rel="nofollow" class="external text" href="https://www.jstor.org/stable/2270177">2270177</a>, <a href="MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=0224460">0224460</a></cite></li></ul>

<ul><li><cite id="CITEREFGladstone1971" class="citation journal cs2">Gladstone, M. D. (1971), "Simplifications of the recursion scheme", The Journal of Symbolic Logic, 36 (4): 653–665, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.2307%2F2272468">10.2307/2272468</a>, <a href="JSTOR_(identifier)" class="mw-redirect" title="JSTOR (identifier)">JSTOR</a> <a rel="nofollow" class="external text" href="https://www.jstor.org/stable/2272468">2272468</a>, <a href="MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=0305993">0305993</a></cite></li></ul>

<ul><li><cite id="CITEREFHartmanis1989" class="citation book cs2"><a href="Juris_Hartmanis" title="Juris Hartmanis">Hartmanis, Juris</a> (1989), "Overview of Computational Complexity Theory", Computational Complexity Theory, Proceedings of Symposia in Applied Mathematics, vol. 38, American Mathematical Society, pp. 1–17, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-8218-0131-4</bdi>, <a href="MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=1020807">1020807</a></cite></li></ul>

<ul><li><cite id="CITEREFKleene1974" class="citation book cs2"><a href="Stephen_Cole_Kleene" title="Stephen Cole Kleene">Kleene, Stephen Cole</a> (1974) [1952], "Chapter XI. General Recursive Functions §57", Introduction to Metamathematics (7th reprint; 2nd ed.), <a href="North-Holland_Publishing_Company" class="mw-redirect" title="North-Holland Publishing Company">North-Holland Publishing Company</a>, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0444100881</bdi>, <a href="OCLC_(identifier)" class="mw-redirect" title="OCLC (identifier)">OCLC</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/oclc/3757798">3757798</a></cite></li></ul>

<ul><li><cite id="CITEREFPlanetMath" class="citation web cs2">PlanetMath, <a rel="nofollow" class="external text" href="https://planetmath.org/primitiverecursivevectorvaluedfunction">"primitive recursive vector-valued function"</a>, retrieved 2025-07-04</cite></li></ul>

<ul><li><cite id="CITEREFRogers1987" class="citation book cs2">Rogers, Hartley Jr. (1987) [1967], Theory of Recursive Functions and Effective Computability (Reprint ed.), <a href="MIT_Press" title="MIT Press">MIT Press</a>, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9780262680523</bdi></cite></li></ul>

<ul><li><cite id="CITEREFRobinson1947" class="citation journal cs2">Robinson, Raphael M. (1947), <a rel="nofollow" class="external text" href="https://doi.org/10.1090%2FS0002-9904-1947-08911-4">"Primitive recursive functions"</a>, Bulletin of the American Mathematical Society, 53 (10): 925–942, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1090%2FS0002-9904-1947-08911-4">10.1090/S0002-9904-1947-08911-4</a>, <a href="MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=0022536">0022536</a></cite></li></ul>

<ul><li><cite id="CITEREFSeverin2008" class="citation journal cs2">Severin, Daniel E. (2008), "Unary primitive recursive functions", The Journal of Symbolic Logic, 73 (4): 1122–1138, <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<a rel="nofollow" class="external text" href="https://arxiv.org/abs/cs/0603063">cs/0603063</a>, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.2178%2Fjsl%2F1230396909">10.2178/jsl/1230396909</a>, <a href="JSTOR_(identifier)" class="mw-redirect" title="JSTOR (identifier)">JSTOR</a> <a rel="nofollow" class="external text" href="https://www.jstor.org/stable/275903221">275903221</a>, <a href="MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=2467207">2467207</a></cite></li></ul>

<ul><li><cite id="CITEREFSoare1987" class="citation book cs2"><a href="Robert_I._Soare" title="Robert I. Soare">Soare, Robert I.</a> (1987), Recursively Enumerable Sets and Degrees, Springer-Verlag, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-387-15299-7</bdi></cite></li></ul>

<ul><li><cite id="CITEREFSoare1996" class="citation journal cs2"><a href="Robert_I._Soare" title="Robert I. Soare">Soare, Robert I.</a> (1996), <a rel="nofollow" class="external text" href="https://scholar.archive.org/work/ruvjr6nkyre4nfxjdme2refpwe">"Computability and recursion"</a>, The Bulletin of Symbolic Logic, 2 (3): 284–321, <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.2307%2F420992">10.2307/420992</a>, <a href="JSTOR_(identifier)" class="mw-redirect" title="JSTOR (identifier)">JSTOR</a> <a rel="nofollow" class="external text" href="https://www.jstor.org/stable/420992">420992</a>, <a href="MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=1416870">1416870</a></cite></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Mathematical_logic344" style="padding:3px"><table class="nowraplinks mw-collapsible mw-collapsed navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Mathematical_logic344" style="font-size:114%;margin:0 4em"><a href="Mathematical_logic" title="Mathematical logic">Mathematical logic</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">General</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Axiom" title="Axiom">Axiom</a>

<li><a href="Cardinality" title="Cardinality">Cardinality</a></li>

<li><a href="First-order_logic" title="First-order logic">First-order logic</a></li>

<li><a href="Formal_proof" title="Formal proof">Formal proof</a></li>

<li><a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics</a></li>

<li><a href="Foundations_of_mathematics" title="Foundations of mathematics">Foundations of mathematics</a></li>

<li><a href="Information_theory" title="Information theory">Information theory</a></li>

<li><a href="Lemma_(mathematics)" title="Lemma (mathematics)">Lemma</a></li>

<li><a href="Logical_consequence" title="Logical consequence">Logical consequence</a></li>

<li><a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a></li>

<li><a href="Theorem" title="Theorem">Theorem</a></li>

<li><a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a></li>

<li><a href="Type_theory" title="Type theory">Type theory</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Theorems (list)  and <a href="Paradoxes_of_set_theory" title="Paradoxes of set theory">paradoxes</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="G%C3%B6del's_completeness_theorem" title="Gödel's completeness theorem">Gödel's completeness</a> and <a href="G%C3%B6del's_incompleteness_theorems" title="Gödel's incompleteness theorems">incompleteness theorems</a></li>

<li><a href="Tarski's_undefinability_theorem" title="Tarski's undefinability theorem">Tarski's undefinability</a></li>

<li><a href="Banach%E2%80%93Tarski_paradox" title="Banach–Tarski paradox">Banach–Tarski paradox</a></li>

<li>Cantor's <a href="Cantor's_theorem" title="Cantor's theorem">theorem,</a> <a href="Cantor's_paradox" title="Cantor's paradox">paradox</a> and <a href="Cantor's_diagonal_argument" title="Cantor's diagonal argument">diagonal argument</a></li>

<li><a href="Compactness_theorem" title="Compactness theorem">Compactness</a></li>

<li><a href="Halting_problem" title="Halting problem">Halting problem</a></li>

<li><a href="Lindstr%C3%B6m's_theorem" title="Lindström's theorem">Lindström's</a></li>

<li><a href="L%C3%B6wenheim%E2%80%93Skolem_theorem" title="Löwenheim–Skolem theorem">Löwenheim–Skolem</a></li>

<li><a href="Russell's_paradox" title="Russell's paradox">Russell's paradox</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Logic" title="Logic">Logics</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th id="Traditional95" scope="row" class="navbox-group" style="width:1%"><a href="Term_logic" title="Term logic">Traditional</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Classical_logic" title="Classical logic">Classical logic</a></li>

<li><a href="Logical_truth" title="Logical truth">Logical truth</a></li>

<li><a href="Tautology_(logic)" title="Tautology (logic)">Tautology</a></li>

<li><a href="Proposition" title="Proposition">Proposition</a></li>

<li><a href="Inference" title="Inference">Inference</a></li>

<li><a href="Logical_equivalence" title="Logical equivalence">Logical equivalence</a></li>

<li><a href="Consistency" title="Consistency">Consistency</a>

<ul><li><a href="Equiconsistency" title="Equiconsistency">Equiconsistency</a></li></ul></li>

<li><a href="Argument" title="Argument">Argument</a></li>

<li><a href="Soundness" title="Soundness">Soundness</a></li>

<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li>

<li><a href="Syllogism" title="Syllogism">Syllogism</a></li>

<li><a href="Square_of_opposition" title="Square of opposition">Square of opposition</a></li>

<li><a href="Venn_diagram" title="Venn diagram">Venn diagram</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Boolean_algebra" title="Boolean algebra">Boolean algebra</a></li>

<li><a href="Boolean_function" title="Boolean function">Boolean functions</a></li>

<li><a href="Logical_connective" title="Logical connective">Logical connectives</a></li>

<li><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional calculus</a></li>

<li><a href="Propositional_formula" title="Propositional formula">Propositional formula</a></li>

<li><a href="Truth_table" title="Truth table">Truth tables</a></li>

<li><a href="Many-valued_logic" title="Many-valued logic">Many-valued logic</a>

<li><a href="Finite-valued_logic" title="Finite-valued logic">finite</a></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Predicate_logic" class="mw-redirect" title="Predicate logic">Predicate</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="First-order_logic" title="First-order logic">First-order</a>

<li><a href="Second-order_logic" title="Second-order logic">Second-order</a>

<ul><li><a href="Monadic_second-order_logic" title="Monadic second-order logic">Monadic</a></li></ul></li>

<li><a href="Higher-order_logic" title="Higher-order logic">Higher-order</a></li>

<li><a href="Fixed-point_logic" title="Fixed-point logic">Fixed-point</a></li>

<li><a href="Quantifier_(logic)" title="Quantifier (logic)">Quantifiers</a></li>

<li><a href="Predicate_(mathematical_logic)" class="mw-redirect" title="Predicate (mathematical logic)">Predicate</a></li>

<li><a href="Monadic_predicate_calculus" title="Monadic predicate calculus">Monadic predicate calculus</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Set_theory" title="Set theory">Set theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Hereditary_set" title="Hereditary set">hereditary</a></li></ul></li>

<li><a href="Class_(set_theory)" title="Class (set theory)">Class</a></li>

<li>(<a href="Urelement" title="Urelement">Ur-</a>)<a href="Element_(mathematics)" title="Element (mathematics)">Element</a></li>

<li><a href="Ordinal_number" title="Ordinal number">Ordinal number</a></li>

<li><a href="Extensionality" title="Extensionality">Extensionality</a></li>

<li><a href="Forcing_(mathematics)" title="Forcing (mathematics)">Forcing</a></li>

<li><a href="Relation_(mathematics)" title="Relation (mathematics)">Relation</a>

<ul><li><a href="Equivalence_relation" title="Equivalence relation">equivalence</a></li>

<li><a href="Partition_of_a_set" title="Partition of a set">partition</a></li></ul></li>

<li>Set operations:

<ul><li><a href="Intersection_(set_theory)" title="Intersection (set theory)">intersection</a></li>

<li><a href="Union_(set_theory)" title="Union (set theory)">union</a></li>

<li><a href="Complement_(set_theory)" title="Complement (set theory)">complement</a></li>

<li><a href="Cartesian_product" title="Cartesian product">Cartesian product</a></li>

<li><a href="Power_set" title="Power set">power set</a></li>

<li><a href="List_of_set_identities_and_relations" title="List of set identities and relations">identities</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Types of <a href="Set_(mathematics)" title="Set (mathematics)">sets</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Countable_set" title="Countable set">Countable</a></li>

<li><a href="Uncountable_set" title="Uncountable set">Uncountable</a></li>

<li><a href="Empty_set" title="Empty set">Empty</a></li>

<li><a href="Inhabited_set" title="Inhabited set">Inhabited</a></li>

<li><a href="Singleton_(mathematics)" title="Singleton (mathematics)">Singleton</a></li>

<li><a href="Finite_set" title="Finite set">Finite</a></li>

<li><a href="Infinite_set" title="Infinite set">Infinite</a></li>

<li><a href="Transitive_set" title="Transitive set">Transitive</a></li>

<li><a href="Ultrafilter_(set_theory)" class="mw-redirect" title="Ultrafilter (set theory)">Ultrafilter</a></li>

<li><a href="Recursive_set" class="mw-redirect" title="Recursive set">Recursive</a></li>

<li><a href="Fuzzy_set" title="Fuzzy set">Fuzzy</a></li>

<li><a href="Universal_set" title="Universal set">Universal</a></li>

<li><a href="Universe_(mathematics)" title="Universe (mathematics)">Universe</a>

<ul><li><a href="Constructible_universe" title="Constructible universe">constructible</a></li>

<li><a href="Grothendieck_universe" title="Grothendieck universe">Grothendieck</a></li>

<li><a href="Von_Neumann_universe" title="Von Neumann universe">Von Neumann</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Map_(mathematics)" title="Map (mathematics)">Maps</a> and <a href="Cardinality" title="Cardinality">cardinality</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Function_(mathematics)" title="Function (mathematics)">Function</a>/<a href="Map_(mathematics)" title="Map (mathematics)">Map</a>

<ul><li><a href="Domain_of_a_function" title="Domain of a function">domain</a></li>

<li><a href="Codomain" title="Codomain">codomain</a></li>

<li><a href="Image_(mathematics)" title="Image (mathematics)">image</a></li></ul></li>

<li><a href="Injective_function" title="Injective function">In</a>/<a href="Surjective_function" title="Surjective function">Sur</a>/<a href="Bijection" title="Bijection">Bi</a>-jection</li>

<li><a href="Schr%C3%B6der%E2%80%93Bernstein_theorem" title="Schröder–Bernstein theorem">Schröder–Bernstein theorem</a></li>

<li><a href="Isomorphism" title="Isomorphism">Isomorphism</a></li>

<li><a href="G%C3%B6del_numbering" title="Gödel numbering">Gödel numbering</a></li>

<li><a href="Enumeration" title="Enumeration">Enumeration</a></li>

<li><a href="Large_cardinal" title="Large cardinal">Large cardinal</a>

<ul><li><a href="Inaccessible_cardinal" title="Inaccessible cardinal">inaccessible</a></li></ul></li>

<li><a href="Aleph_number" title="Aleph number">Aleph number</a></li>

<li><a href="Operation_(mathematics)" title="Operation (mathematics)">Operation</a>

<ul><li><a href="Binary_operation" title="Binary operation">binary</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Set theories</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Zermelo–Fraenkel</a>

<ul><li><a href="Axiom_of_choice" title="Axiom of choice">axiom of choice</a></li>

<li><a href="Continuum_hypothesis" title="Continuum hypothesis">continuum hypothesis</a></li></ul></li>

<li><a href="General_set_theory" title="General set theory">General</a></li>

<li><a href="Kripke%E2%80%93Platek_set_theory" title="Kripke–Platek set theory">Kripke–Platek</a></li>

<li><a href="Morse%E2%80%93Kelley_set_theory" title="Morse–Kelley set theory">Morse–Kelley</a></li>

<li><a href="Naive_set_theory" title="Naive set theory">Naive</a></li>

<li><a href="New_Foundations" title="New Foundations">New Foundations</a></li>

<li><a href="Tarski%E2%80%93Grothendieck_set_theory" title="Tarski–Grothendieck set theory">Tarski–Grothendieck</a></li>

<li><a href="Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory" title="Von Neumann–Bernays–Gödel set theory">Von Neumann–Bernays–Gödel</a></li>

<li><a href="Ackermann_set_theory" title="Ackermann set theory">Ackermann</a></li>

<li><a href="Constructive_set_theory" title="Constructive set theory">Constructive</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Formal_system" title="Formal system">Formal systems</a> (<a href="List_of_formal_systems" title="List of formal systems">list</a>), <a href="Formal_language" title="Formal language">language</a> and <a href="Syntax_(logic)" title="Syntax (logic)">syntax</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Alphabet_(formal_languages)" title="Alphabet (formal languages)">Alphabet</a></li>

<li><a href="Arity" title="Arity">Arity</a></li>

<li><a href="Automata_theory" title="Automata theory">Automata</a></li>

<li><a href="Axiom_schema" title="Axiom schema">Axiom schema</a></li>

<li><a href="Expression_(mathematics)" title="Expression (mathematics)">Expression</a>

<ul><li><a href="Ground_expression" title="Ground expression">ground</a></li></ul></li>

<li><a href="Extension_by_new_constant_and_function_names" title="Extension by new constant and function names">Extension</a>

<ul><li><a href="Extension_by_definitions" class="mw-redirect" title="Extension by definitions">by definition</a></li>

<li><a href="Conservative_extension" title="Conservative extension">conservative</a></li></ul></li>

<li><a href="Finitary_relation" title="Finitary relation">Relation</a></li>

<li><a href="Formation_rule" title="Formation rule">Formation rule</a></li>

<li><a href="Formal_grammar" title="Formal grammar">Grammar</a></li>

<li><a href="Well-formed_formula" title="Well-formed formula">Formula</a>

<ul><li><a href="Atomic_formula" title="Atomic formula">atomic</a></li>

<li><a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">closed</a></li>

<li><a href="Ground_formula" class="mw-redirect" title="Ground formula">ground</a></li>

<li><a href="Free_variables_and_bound_variables" title="Free variables and bound variables">Free/bound variable</a></li>

<li><a href="Formal_language" title="Formal language">Language</a></li>

<li><a href="Metalanguage" title="Metalanguage">Metalanguage</a></li>

<li><a href="Logical_connective" title="Logical connective">Logical connective</a>

<li><a href="Predicate_(mathematical_logic)" class="mw-redirect" title="Predicate (mathematical logic)">Predicate</a>

<ul><li><a href="Functional_predicate" title="Functional predicate">functional</a></li>

<li><a href="Predicate_variable" title="Predicate variable">variable</a></li>

<li><a href="Propositional_variable" title="Propositional variable">propositional variable</a></li></ul></li>

<li><a href="Formal_proof" title="Formal proof">Proof</a></li>

<li><a href="Quantifier_(logic)" title="Quantifier (logic)">Quantifier</a>

<li><a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">Sentence</a>

<ul><li><a href="Atomic_sentence" title="Atomic sentence">atomic</a></li>

<li><a href="Spectrum_of_a_sentence" title="Spectrum of a sentence">spectrum</a></li></ul></li>

<li><a href="Signature_(logic)" title="Signature (logic)">Signature</a></li>

<li><a href="String_(formal_languages)" class="mw-redirect" title="String (formal languages)">String</a></li>

<li><a href="Substitution_(logic)" title="Substitution (logic)">Substitution</a></li>

<li><a href="Symbol_(formal)" title="Symbol (formal)">Symbol</a>

<ul><li><a href="Uninterpreted_function" title="Uninterpreted function">function</a></li>

<li><a href="Logical_constant" title="Logical constant">logical/constant</a></li>

<li><a href="Non-logical_symbol" title="Non-logical symbol">non-logical</a></li>

<li><a href="Variable_(mathematics)" title="Variable (mathematics)">variable</a></li></ul></li>

<li><a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Example <a href="Axiomatic_system" title="Axiomatic system">axiomatic systems</a> (<a href="List_of_first-order_theories" title="List of first-order theories">list</a>)</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li>of <a href="True_arithmetic" title="True arithmetic">arithmetic</a>:

<ul><li><a href="Peano_axioms" title="Peano axioms">Peano</a></li>

<li><a href="Second-order_arithmetic" title="Second-order arithmetic">second-order</a></li>

<li><a href="Elementary_function_arithmetic" title="Elementary function arithmetic">elementary function</a></li>

<li><a href="Primitive_recursive_arithmetic" title="Primitive recursive arithmetic">primitive recursive</a></li>

<li><a href="Robinson_arithmetic" title="Robinson arithmetic">Robinson</a></li>

<li><a href="Skolem_arithmetic" title="Skolem arithmetic">Skolem</a></li></ul></li>

<li>of the <a href="Construction_of_the_real_numbers" title="Construction of the real numbers">real numbers</a>

<ul><li><a href="Tarski's_axiomatization_of_the_reals" title="Tarski's axiomatization of the reals">Tarski's axiomatization</a></li></ul></li>

<li>of <a href="Axiomatization_of_Boolean_algebras" class="mw-redirect" title="Axiomatization of Boolean algebras">Boolean algebras</a>

<ul><li><a href="Boolean_algebras_canonically_defined" title="Boolean algebras canonically defined">canonical</a></li>

<li><a href="Minimal_axioms_for_Boolean_algebra" title="Minimal axioms for Boolean algebra">minimal axioms</a></li></ul></li>

<li>of <a href="Foundations_of_geometry" title="Foundations of geometry">geometry</a>:

<ul><li><a href="Euclidean_geometry" title="Euclidean geometry">Euclidean</a>:

<ul><li><a href="Euclid's_Elements" title="Euclid's Elements">Elements</a></li>

<li><a href="Hilbert's_axioms" title="Hilbert's axioms">Hilbert's</a></li>

<li><a href="Tarski's_axioms" title="Tarski's axioms">Tarski's</a></li></ul></li>

<li><a href="Non-Euclidean_geometry" title="Non-Euclidean geometry">non-Euclidean</a></li></ul></li></ul>

<ul><li><a href="Principia_Mathematica" title="Principia Mathematica">Principia Mathematica</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Proof_theory" title="Proof theory">Proof theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Formal_proof" title="Formal proof">Formal proof</a></li>

<li><a href="Natural_deduction" title="Natural deduction">Natural deduction</a></li>

<li><a href="Logical_consequence" title="Logical consequence">Logical consequence</a></li>

<li><a href="Rule_of_inference" title="Rule of inference">Rule of inference</a></li>

<li><a href="Sequent_calculus" title="Sequent calculus">Sequent calculus</a></li>

<li><a href="Theorem" title="Theorem">Theorem</a></li>

<li><a href="Formal_system" title="Formal system">Systems</a>

<ul><li><a href="Axiomatic_system" title="Axiomatic system">axiomatic</a></li>

<li><a href="Deductive_system" class="mw-redirect" title="Deductive system">deductive</a></li>

<li><a href="Hilbert_system" title="Hilbert system">Hilbert</a>

<li><a href="Complete_theory" title="Complete theory">Complete theory</a></li>

<li><a href="Independence_(mathematical_logic)" title="Independence (mathematical logic)">Independence</a> (<a href="List_of_statements_independent_of_ZFC" title="List of statements independent of ZFC">from ZFC</a>)</li>

<li><a href="Proof_of_impossibility" title="Proof of impossibility">Proof of impossibility</a></li>

<li><a href="Ordinal_analysis" title="Ordinal analysis">Ordinal analysis</a></li>

<li><a href="Reverse_mathematics" title="Reverse mathematics">Reverse mathematics</a></li>

<li><a href="Self-verifying_theories" title="Self-verifying theories">Self-verifying theories</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Model_theory" title="Model theory">Model theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Interpretation_(logic)" title="Interpretation (logic)">Interpretation</a>

<ul><li><a href="Interpretation_function" class="mw-redirect" title="Interpretation function">function</a></li>

<li><a href="Interpretation_(model_theory)" title="Interpretation (model theory)">of models</a></li></ul></li>

<li><a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a>

<ul><li><a href="Elementary_equivalence" title="Elementary equivalence">equivalence</a></li>

<li><a href="Finite_model_theory" title="Finite model theory">finite</a></li>

<li><a href="Saturated_model" title="Saturated model">saturated</a></li>

<li><a href="Spectrum_of_a_theory" title="Spectrum of a theory">spectrum</a></li>

<li><a href="Substructure_(mathematics)" title="Substructure (mathematics)">submodel</a></li></ul></li>

<li><a href="Non-standard_model" title="Non-standard model">Non-standard model</a>

<ul><li><a href="Non-standard_model_of_arithmetic" title="Non-standard model of arithmetic">of arithmetic</a></li></ul></li>

<li><a href="Diagram_(mathematical_logic)" title="Diagram (mathematical logic)">Diagram</a>

<ul><li><a href="Elementary_diagram" title="Elementary diagram">elementary</a></li></ul></li>

<li><a href="Categorical_theory" title="Categorical theory">Categorical theory</a></li>

<li><a href="Model_complete_theory" title="Model complete theory">Model complete theory</a></li>

<li><a href="Satisfiability" title="Satisfiability">Satisfiability</a></li>

<li><a href="Semantics_of_logic" title="Semantics of logic">Semantics of logic</a></li>

<li><a href="Strength_(mathematical_logic)" title="Strength (mathematical logic)">Strength</a></li>

<li><a href="Theories_of_truth" class="mw-redirect" title="Theories of truth">Theories of truth</a>

<ul><li><a href="Semantic_theory_of_truth" title="Semantic theory of truth">semantic</a></li>

<li><a href="Tarski's_theory_of_truth" class="mw-redirect" title="Tarski's theory of truth">Tarski's</a></li>

<li><a href="Kripke's_theory_of_truth" class="mw-redirect" title="Kripke's theory of truth">Kripke's</a></li></ul></li>

<li><a href="T-schema" title="T-schema">T-schema</a></li>

<li><a href="Transfer_principle" title="Transfer principle">Transfer principle</a></li>

<li><a href="Truth_predicate" title="Truth predicate">Truth predicate</a></li>

<li><a href="Truth_value" title="Truth value">Truth value</a></li>

<li><a href="Ultraproduct" title="Ultraproduct">Ultraproduct</a></li>

<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computability_theory" title="Computability theory">Computability theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Church_encoding" title="Church encoding">Church encoding</a></li>

<li><a href="Church%E2%80%93Turing_thesis" title="Church–Turing thesis">Church–Turing thesis</a></li>

<li><a href="Computably_enumerable_set" title="Computably enumerable set">Computably enumerable</a></li>

<li><a href="Computable_function" title="Computable function">Computable function</a></li>

<li><a href="Computable_set" title="Computable set">Computable set</a></li>

<li><a href="Decision_problem" title="Decision problem">Decision problem</a>

<ul><li><a href="Decidability_(logic)" title="Decidability (logic)">decidable</a></li>

<li><a href="Undecidable_problem" title="Undecidable problem">undecidable</a></li>

<li><a href="P_versus_NP_problem" title="P versus NP problem">P versus NP problem</a></li></ul></li>

<li><a href="Kolmogorov_complexity" title="Kolmogorov complexity">Kolmogorov complexity</a></li>

<li><a href="Lambda_calculus" title="Lambda calculus">Lambda calculus</a></li>

<li><a href="Recursion" title="Recursion">Recursion</a></li>

<li><a href="Recursive_set" class="mw-redirect" title="Recursive set">Recursive set</a></li>

<li><a href="Turing_machine" title="Turing machine">Turing machine</a></li>

<li><a href="Type_theory" title="Type theory">Type theory</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Abstract_logic" title="Abstract logic">Abstract logic</a></li>

<li><a href="Algebraic_logic" title="Algebraic logic">Algebraic logic</a></li>

<li><a href="Automated_theorem_proving" title="Automated theorem proving">Automated theorem proving</a></li>

<li><a href="Category_theory" title="Category theory">Category theory</a></li>

<li><a href="Concrete_category" title="Concrete category">Concrete</a>/<a href="Category_(mathematics)" title="Category (mathematics)">Abstract category</a></li>

<li><a href="Category_of_sets" title="Category of sets">Category of sets</a></li>

<li><a href="History_of_logic" title="History of logic">History of logic</a></li>

<li><a href="History_of_mathematical_logic" class="mw-redirect" title="History of mathematical logic">History of mathematical logic</a>

<ul><li><a href="Timeline_of_mathematical_logic" title="Timeline of mathematical logic">timeline</a></li></ul></li>

<li><a href="Logicism" title="Logicism">Logicism</a></li>

<li><a href="Mathematical_object" title="Mathematical object">Mathematical object</a></li>

<li><a href="Philosophy_of_mathematics" title="Philosophy of mathematics">Philosophy of mathematics</a></li>

<li><a href="Supertask" title="Supertask">Supertask</a></li></ul>

</div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div> <a href="Portal%3AMathematics" title="Portal:Mathematics">Mathematics portal</a></div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-07-30" href="https://en.wikipedia.org/wiki/?title=Primitive_recursive_function&oldid=1303327175">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>